diff --git a/interpreter/examples/utests/extatoms01 b/interpreter/examples/utests/extatoms01 new file mode 100644 index 000000000..32de9ac72 --- /dev/null +++ b/interpreter/examples/utests/extatoms01 @@ -0,0 +1,39 @@ +(def Fa (normalize 'level 1 [ x /= 12 /\ [y > _root_2 (x - 1)(y^2 - 2 x + 3)]])) +(def Faexpected [x - 12 /= 0 /\ x - 1 /= 0 /\ y > _root_2 y^2 - 2 x + 3]) +(def resa (if (equal? Fa Faexpected) "pass" "fail")) +(display resa " : test extatoms01 - a\n") + +(def Fb (normalize 'level 1 [y > _root_2 (x - 1)(y^2 - 2 x + 3)])) +(def Fbexpected [x - 1 /= 0 /\ y > _root_2 y^2 - 2 x + 3]) +(def resb (if (equal? Fb Fbexpected) "pass" "fail")) +(display resb " : test extatoms01 - b\n") + +(def Fc (qepcad-api-call [ex y[ x <= 10 /\ [y > _root_2 (x - 5)(y^2 - 2 x + 3)]]])) +(def Fcexpected [x - 10 <= 0 /\ x - 5 /= 0 /\ 2 x - 3 > 0]) +(def resc (if (equal? Fc Fcexpected) "pass" "fail")) +(display resc " : test extatoms01 - c\n") + +(def Fd (qepcad-qe [ex y[ x <= 10 /\ [y > _root_2 (x - 5)(y^2 - 2 x + 3)]]])) +(def Fdexpected [x - 10 <= 0 /\ x - 5 /= 0 /\ 2 x - 3 > 0]) +(def resd (if (equal? Fd Fdexpected) "pass" "fail")) +(display resd " : test extatoms01 - d\n") + +(def Fe (get (qepcad-sat [ x <= 10 /\ [y > _root_2 (x - 5)(y^2 - 2 x + 3)]]) 0)) +(def Feexpected 'SAT) +(def rese (if (equal? Fe Feexpected) "pass" "fail")) +(display rese " : test extatoms01 - e\n") + +(display (if (equal? (normalize 'level 1 [ y > _root_1 x + 1 ]) [false]) "pass" "fail") " : test extatoms01 - f\n") + +(display (if (equal? (normalize 'level 1 [ y > _root_1 y + 1 ]) [ y > _root_1 y + 1 ]) "pass" "fail") " : test extatoms01 - g\n") + +(display (if (equal? (normalize 'level 1 [ y > _root_1 x^2 (y + 1)^2 ]) [ x /= 0 /\ y > _root_1 y + 1 ]) "pass" "fail") " : test extatoms01 - h\n") + +(def Fi (normalize 'level 1 (evalf 'x 1 [ex z[ z > _root_2 (x - y + 1) (x z^2 - x - y + 1)]]))) +(def Fiexpected [ex z[y - 2 /= 0 /\ z > _root_2 z^2 - y]]) +(def resi (if (equal? Fi Fiexpected) "pass" "fail")) +(display resi " : test extatoms01 - i\n") + + + + diff --git a/interpreter/examples/utests/smt/smt009.smt2 b/interpreter/examples/utests/smt/smt009.smt2 new file mode 100644 index 000000000..616b707cf --- /dev/null +++ b/interpreter/examples/utests/smt/smt009.smt2 @@ -0,0 +1,9 @@ +(set-info :status unsat) +(set-logic QF_NRA) +(set-info :source | Simple test example.|) +(set-info :smt-lib-version 2.0) +(declare-fun x () Real) +(declare-fun y () Real) +(assert (< x 1)) +(assert (and (> (/ y 3) 2) (<= (/ 1 (+ x (/ 1 (- y 2)))) 3))) +(checksat) diff --git a/interpreter/src/formula/formmanip.cpp b/interpreter/src/formula/formmanip.cpp index 988f77881..4144e3e40 100755 --- a/interpreter/src/formula/formmanip.cpp +++ b/interpreter/src/formula/formmanip.cpp @@ -440,6 +440,7 @@ class GetFreeVars : public TFPolyFun VarSet res; void action(TConstObj* p) { res = p->getVars(); } void action(TAtomObj* p) { res = p->getVars(); } + void action(TExtAtomObj* p) { res = p->getVars(); } void action(TAndObj* p) { VarSet V; diff --git a/interpreter/src/formula/normalize.cpp b/interpreter/src/formula/normalize.cpp index 81473f797..c4968339c 100755 --- a/interpreter/src/formula/normalize.cpp +++ b/interpreter/src/formula/normalize.cpp @@ -91,6 +91,42 @@ namespace tarski { return true; } + + // The RHS content is thrown out. All factors made multiplicity one. + // Formula: z sigma _root_k p + // If p is zero or constant or if the sum of degrees in z of all factors is less than k, formula is false. + // if the factors of p are f1,..., fm and g1,...,gm where the fi's have positive degree in z and gj's not, + // then g1 /= 0 /\ ... /\ gm /= 0 /\ z relop _root_k f1 * ... fm + bool level1_extatom(TExtAtomRef A, TAndRef C) + { + VarSet z = A->getLHSVar(); + vector G; + FactRef F = new FactObj(A->getPolyManagerPtr()); + int degreeSum = 0; + for(auto itr = A->factorsBegin(); itr != A->factorsEnd(); ++itr) { + IntPolyRef q = itr->first; + int dz = q->degree(z); + if (dz > 0) { + degreeSum += dz; + F->addFactor(q,1); + } + else + G.push_back(q); + } + if (degreeSum < A->getRootIndex()) + return false; + + for(int i = 0; i < G.size(); i++) { + FactRef f = new FactObj(A->getPolyManagerPtr()); + f->addFactor(G[i],1); + C->conjuncts.insert(new TAtomObj(f,NEOP)); + } + C->conjuncts.insert(new TExtAtomObj(z,A->getRelop(),A->getRootIndex(),F)); + + return true; + } + + TFormRef level1_and(TAndRef Cinit, TAtomRef* ptr = NULL) { TAndRef Cfinal = new TAndObj; @@ -98,14 +134,23 @@ namespace tarski { switch ((*itr)->constValue()) { case FALSE: return new TConstObj(FALSE); break; case TRUE: break; - default: - if (level1_atom(*itr,Cfinal) == false) + default: { + bool res = true; + switch((*itr)->getTFType()) { + case TF_ATOM: res = level1_atom(*itr,Cfinal); break; + case TF_EXTATOM: res = level1_extatom(*itr,Cfinal); break; + default: + throw TarskiException("In Level1 normalization, expected atomic formula!"); + break; + } + if (res == false) { if (ptr != NULL) { (*ptr) = *itr; } return new TConstObj(FALSE); } break; } + } } if (0) { // stats gathering ... temporary stuff! @@ -114,7 +159,6 @@ namespace tarski { cout << endl << endl; } - return Cfinal; } @@ -122,10 +166,12 @@ namespace tarski { { TAndRef A = asa(F); if (A.is_null()) - { - TAtomRef T = asa(F); - if (!T.is_null()) { A = new TAndObj; A->conjuncts.insert(T); } - } + { + A = new TAndObj(); + A->AND(F); + // TAtomRef T = asa(F); + // if (!T.is_null()) { A = new TAndObj; A->conjuncts.insert(T); } + } if (!A.is_null()) return level1_and(A,ptr); else return F; } @@ -268,35 +314,35 @@ namespace tarski { map > whatWeKnow; set multiFactorAtoms; for(set::iterator itr = Cinit->conjuncts.begin(); f && itr != Cinit->conjuncts.end(); ++itr) - { - TAtomRef A = asa(*itr); if (A.is_null()) { cerr << "Non-atom in conjunct!" << endl; exit(1); } - for(map::iterator itrF = A->factorsBegin(); f && itrF != A->factorsEnd(); ++itrF) - f = addInfoTo(whatWeKnow,A,itrF->first,N); - if (A->F->numFactors() > 1) - multiFactorAtoms.insert(A); - } + { + TAtomRef A = asa(*itr); if (A.is_null()) { cerr << "Non-atom in conjunct!" << endl; exit(1); } + for(map::iterator itrF = A->factorsBegin(); f && itrF != A->factorsEnd(); ++itrF) + f = addInfoTo(whatWeKnow,A,itrF->first,N); + if (A->F->numFactors() > 1) + multiFactorAtoms.insert(A); + } if (!f) { return new TConstObj(FALSE); } // Set up P, the vector of factors vector P(N); for(map >::iterator itr = whatWeKnow.begin(); itr != whatWeKnow.end(); ++itr) - { - P[itr->second.second].f = itr->first; - P[itr->second.second].relop = itr->second.first; - } + { + P[itr->second.second].f = itr->first; + P[itr->second.second].relop = itr->second.first; + } //---------- LEVEL 3 SECTION ------------------------------- // which tries to deduce signs of factors by what it knows of the signs of vars VarKeyedMap varSign(ALOP); if (l3flags) - { - TConstRef res = levelThreePart(P,varSign,ptrPM); - if (!res.is_null()) - { - if (verbose) { cout << "Level 3 normalization found conflict in "; Cinit->write(); cout << endl; } - return res; - } + { + TConstRef res = levelThreePart(P,varSign,ptrPM); + if (!res.is_null()) + { + if (verbose) { cout << "Level 3 normalization found conflict in "; Cinit->write(); cout << endl; } + return res; } + } if (l3flags & nf_ded_strengthenings) { for(unsigned int i = 0; i < P.size(); ++i) P[i].relop &= P[i].l3dedRelop; } //------------- LEVEL 4 SECTION -------------------------------- @@ -305,10 +351,10 @@ namespace tarski { // We must be careful about linear univariate polynomials, however, since they // might be the basis for a decision about the sign of a variable! if (l3flags && l4flags) - { - TConstRef res = levelFourPart(P,varSign,ptrPM,Cinit,l4flags); - if (!res.is_null()) return res; - } + { + TConstRef res = levelFourPart(P,varSign,ptrPM,Cinit,l4flags); + if (!res.is_null()) return res; + } if (l4flags & nf_ded_strengthenings) { for(unsigned int i = 0; i < P.size(); ++i) P[i].relop &= P[i].l4dedRelop; } //------- Simplfify the multiFactorAtoms if possible ---------------- @@ -317,104 +363,104 @@ namespace tarski { vector A(multiFactorAtoms.size()); int M = 0; // Eventually set to the size of A, also used for assigning indices for(set::iterator itr = multiFactorAtoms.begin(); itr != multiFactorAtoms.end(); ++itr) + { + Q.push(M); + A[M].in_queue = true; + A[M].relop = (*itr)->relop; + for(map::iterator itrF = (*itr)->factorsBegin(); f && itrF != (*itr)->factorsEnd(); ++itrF) { - Q.push(M); - A[M].in_queue = true; - A[M].relop = (*itr)->relop; - for(map::iterator itrF = (*itr)->factorsBegin(); f && itrF != (*itr)->factorsEnd(); ++itrF) - { - int indexInP = whatWeKnow[itrF->first].second; - A[M].push_back(pair(indexInP,itrF->second)); - P[indexInP].mfaIndices.insert(M); - } - ++M; + int indexInP = whatWeKnow[itrF->first].second; + A[M].push_back(pair(indexInP,itrF->second)); + P[indexInP].mfaIndices.insert(M); } + ++M; + } // Simplification loop! Note A[i].relop == ALOP means it's been simplified away to TRUE while (!Q.empty()) + { + // Dequeue i and process multi-factor atom A[i] + int i = Q.front(); Q.pop(); A[i].in_queue = false; + int nf = A[i].size(); + int strengthencount = 0; + for(int j = 0; j < nf; ++j) { - // Dequeue i and process multi-factor atom A[i] - int i = Q.front(); Q.pop(); A[i].in_queue = false; - int nf = A[i].size(); - int strengthencount = 0; - for(int j = 0; j < nf; ++j) - { - int k = A[i][j].first; - int factorRelop = P[k].relop & P[k].l3dedRelop & P[k].l4dedRelop; // Strongest relop we know! - switch(ACTIONS [A[i].relop] [A[i][j].second] [factorRelop]) - { - case REP_W_TRUE: - { for(int k = 0; k < nf; ++k) P[A[i][k].first].mfaIndices.erase(i); nf = 0; A[i].relop = NEOP; }break; - case REP_W_FALSE: - nf = 0; A[i].relop = EQOP; break; - case REMOVE_FACT: - P[A[i][j].first].mfaIndices.erase(i); --nf; swap(A[i][j],A[i][nf]); --j; break; - case REM_W_SWAP: - P[A[i][j].first].mfaIndices.erase(i); - --nf; swap(A[i][j],A[i][nf]); --j; A[i].relop = reverseRelop(A[i].relop); break; - case ALLOWS_STR: ++strengthencount; break; - case DO_NOTHING: break; - case IMPOSSIBLE: - cerr << "P[" << k << "] = "; P[k].f->write(*ptrPM); cerr << endl; - cerr << P[k].relop << P[k].l3dedRelop << P[k].l4dedRelop << endl; - cerr << A[i].relop << ' ' << A[i][j].second << ' ' << factorRelop << " : "; - cerr << "Norm2 impossible case reached!" << endl; exit(1); break; - } - } - // Strenghten <= to < or >= to > if allowed. - if (nf > 0 && strengthencount == nf) { - if (A[i].relop == GEOP) A[i].relop = GTOP; - else if (A[i].relop == LEOP) A[i].relop = LTOP; } - - // If A[i] after processing consists of 0 or 1 atom, deal with it! - if (nf == 0 && (A[i].relop & GTOP)) - A[i].relop = (EQOP|NEOP); - else if (nf == 0) - return new TConstObj(FALSE); - else if (nf == 1) - { - int k = A[i][0].first, relop = A[i].relop; - P[k].mfaIndices.erase(i); - if (A[i][0].second == 2) { - if (relop == GEOP) relop = (EQOP|NEOP); - else relop = EQOP; - } - if (P[k].relop != (P[k].relop & relop)) - { - P[k].relop &= relop; - for(set::iterator itr = P[k].mfaIndices.begin(); itr != P[k].mfaIndices.end(); ++itr) - if (!A[*itr].in_queue) { Q.push(*itr); A[*itr].in_queue = true; } - } - } - A[i].resize(nf); + int k = A[i][j].first; + int factorRelop = P[k].relop & P[k].l3dedRelop & P[k].l4dedRelop; // Strongest relop we know! + switch(ACTIONS [A[i].relop] [A[i][j].second] [factorRelop]) + { + case REP_W_TRUE: + { for(int k = 0; k < nf; ++k) P[A[i][k].first].mfaIndices.erase(i); nf = 0; A[i].relop = NEOP; }break; + case REP_W_FALSE: + nf = 0; A[i].relop = EQOP; break; + case REMOVE_FACT: + P[A[i][j].first].mfaIndices.erase(i); --nf; swap(A[i][j],A[i][nf]); --j; break; + case REM_W_SWAP: + P[A[i][j].first].mfaIndices.erase(i); + --nf; swap(A[i][j],A[i][nf]); --j; A[i].relop = reverseRelop(A[i].relop); break; + case ALLOWS_STR: ++strengthencount; break; + case DO_NOTHING: break; + case IMPOSSIBLE: + cerr << "P[" << k << "] = "; P[k].f->write(*ptrPM); cerr << endl; + cerr << P[k].relop << P[k].l3dedRelop << P[k].l4dedRelop << endl; + cerr << A[i].relop << ' ' << A[i][j].second << ' ' << factorRelop << " : "; + cerr << "Norm2 impossible case reached!" << endl; exit(1); break; + } } + // Strenghten <= to < or >= to > if allowed. + if (nf > 0 && strengthencount == nf) { + if (A[i].relop == GEOP) A[i].relop = GTOP; + else if (A[i].relop == LEOP) A[i].relop = LTOP; } + + // If A[i] after processing consists of 0 or 1 atom, deal with it! + if (nf == 0 && (A[i].relop & GTOP)) + A[i].relop = (EQOP|NEOP); + else if (nf == 0) + return new TConstObj(FALSE); + else if (nf == 1) + { + int k = A[i][0].first, relop = A[i].relop; + P[k].mfaIndices.erase(i); + if (A[i][0].second == 2) { + if (relop == GEOP) relop = (EQOP|NEOP); + else relop = EQOP; + } + if (P[k].relop != (P[k].relop & relop)) + { + P[k].relop &= relop; + for(set::iterator itr = P[k].mfaIndices.begin(); itr != P[k].mfaIndices.end(); ++itr) + if (!A[*itr].in_queue) { Q.push(*itr); A[*itr].in_queue = true; } + } + } + A[i].resize(nf); + } //------- Reconstruct formula------------------------------ // Add all the single factor atoms. TAndRef Res = new TAndObj; for(unsigned int i = 0; i < P.size(); ++i) - { - bool implicit = false; - if (P[i].relop == NEOP) - { - for(set::iterator itr = P[i].mfaIndices.begin(); !implicit && itr != P[i].mfaIndices.end(); ++itr) - implicit = ((A[*itr].relop & EQOP) == 0); - } - if (P[i].relop != ALOP && !implicit && !((l3flags & nf_ded_implications) && P[i].implied)) - Res->AND(makeAtom(*ptrPM,P[i].f,P[i].relop)); + { + bool implicit = false; + if (P[i].relop == NEOP) + { + for(set::iterator itr = P[i].mfaIndices.begin(); !implicit && itr != P[i].mfaIndices.end(); ++itr) + implicit = ((A[*itr].relop & EQOP) == 0); } + if (P[i].relop != ALOP && !implicit && !((l3flags & nf_ded_implications) && P[i].implied)) + Res->AND(makeAtom(*ptrPM,P[i].f,P[i].relop)); + } // Add all the multi-factor atoms. for(unsigned int i = 0; i < A.size(); ++i) - { - if (A[i].relop == (EQOP|NEOP)) continue; - TAtomRef newA = new TAtomObj(*ptrPM); - newA->relop = A[i].relop; - for(unsigned int j = 0; j < A[i].size(); ++j) - newA->F->addFactor(P[A[i][j].first].f,A[i][j].second); - Res->AND(newA); - } + { + if (A[i].relop == (EQOP|NEOP)) continue; + TAtomRef newA = new TAtomObj(*ptrPM); + newA->relop = A[i].relop; + for(unsigned int j = 0; j < A[i].size(); ++j) + newA->F->addFactor(P[A[i][j].first].f,A[i][j].second); + Res->AND(newA); + } // Deal with the possiblity that we end up with one atom if (Res->size() == 0) diff --git a/interpreter/src/formula/normalize.h b/interpreter/src/formula/normalize.h index 3536dd468..107a3130e 100644 --- a/interpreter/src/formula/normalize.h +++ b/interpreter/src/formula/normalize.h @@ -115,7 +115,10 @@ class RawNormalizer : public TFPolyFun RawNormalizer(Normalizer* p) { normp = p; } void action(TConstObj* p) { res = p; } void action(TAtomObj* p) { res = normp->normalize(p); } - void action(TExtAtomObj* p) { throw TarskiException("RawNormalizer does not support _root_ expressions."); } + void action(TExtAtomObj* p) { + res = normp->normalize(p); + //throw TarskiException("RawNormalizer does not support _root_ expressions."); + } void action(TAndObj* p) { // 1: split into two conjunctions - pure atomic formulas, and non-pure atomic formulas diff --git a/interpreter/src/shell/einterpreter.cpp b/interpreter/src/shell/einterpreter.cpp index 2d1ca9a5d..378caf553 100644 --- a/interpreter/src/shell/einterpreter.cpp +++ b/interpreter/src/shell/einterpreter.cpp @@ -382,7 +382,7 @@ class CommNormalize : public EICommand R(F); return new TarObj(R.getRes()); } - if (t->val == "level") + else if (t->val == "level") { Normalizer* p = NULL; switch(k->numerator()) @@ -400,7 +400,7 @@ class CommNormalize : public EICommand return new TarObj(R.getRes()); } else - return new ErrObj("Error in normtest: unknown norm type '" + t->val + "'."); + return new ErrObj("Error in normalize: unknown norm type '" + t->val + "'."); } string testArgs(vector &args) { @@ -413,7 +413,7 @@ class CommNormalize : public EICommand { return "(normalize F), where F is a Tarski Formula, returns\ a Tarski Formula resulting from applying the standard normalizer to F, or\ -(normtest t k F), where F is a Tarski Formula, returns\ +(normalize t k F), where F is a Tarski Formula, returns\ a Tarski Formula resulting from applying a normalizer of type t \ with normalization level k to F. Supported types are 'raw or 'level.\ Values for 'level are 1, 2, 3, 4 or 15."; diff --git a/interpreter/src/shell/qepcad-inter/qepcad-api.cpp b/interpreter/src/shell/qepcad-inter/qepcad-api.cpp index 1467a2d07..39383385b 100644 --- a/interpreter/src/shell/qepcad-inter/qepcad-api.cpp +++ b/interpreter/src/shell/qepcad-inter/qepcad-api.cpp @@ -101,7 +101,8 @@ namespace tarski { // Do basic normalization to get rid of boolean constants, which qepcad // doesn't understand. - RawNormalizer R(defaultNormalizer); + Level1 basicNormalizer; + RawNormalizer R(basicNormalizer); R(T); T = R.getRes(); diff --git a/interpreter/src/shell/schemish.h b/interpreter/src/shell/schemish.h index 517821a3e..3a807d794 100644 --- a/interpreter/src/shell/schemish.h +++ b/interpreter/src/shell/schemish.h @@ -266,11 +266,15 @@ class TarObj: public SObj // there's some efficiency to it. TarRef y = x->tar(); if (y.is_null()) { return new BooObj(false); } - TFormRef A; { RawNormalizer R(defaultNormalizer); R(this->val); A = R.getRes(); } - TFormRef B; { RawNormalizer R(defaultNormalizer); R(y->val); B = R.getRes(); } + Level1 basicNormalizer; + TFormRef A; { RawNormalizer R(basicNormalizer); R(this->val); A = R.getRes(); } + TFormRef B; { RawNormalizer R(basicNormalizer); R(y->val); B = R.getRes(); } + // A->write(true); cerr << endl; + // B->write(true); cerr << endl; + // I think I need the 'true' argument to make this work right! std::ostringstream s1, s2; - PushOutputContext(s1); A->write(); PopOutputContext(); - PushOutputContext(s2); B->write(); PopOutputContext(); + PushOutputContext(s1); A->write(true); PopOutputContext(); + PushOutputContext(s2); B->write(true); PopOutputContext(); return new BooObj(s1.str() == s2.str()); } }; diff --git a/qesource/extensions/sfext/minhit/MINHITSET.c b/qesource/extensions/sfext/minhit/MINHITSET.c index 0cde11071..90fdf7c15 100644 --- a/qesource/extensions/sfext/minhit/MINHITSET.c +++ b/qesource/extensions/sfext/minhit/MINHITSET.c @@ -23,6 +23,10 @@ Word MINHITSET(Word A, Word B) { Word L,As,C,Cp,p,Ap,T,s; + /* SWRITE("In MINHITSET\n"); */ + /* SWRITE("A = "); OWRITE(A); SWRITE("\n"); */ + /* SWRITE("B = "); OWRITE(B); SWRITE("\n"); */ + Step1: /* Quick decisions. */ if (A == NIL) return (NIL); if ((B == 0) || (FIRST(A) == NIL)) return (MC_FAIL);