Seems to be working better <http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3749&category=&p=5&reference_id=3739>, and should fix the failing cases in the regressions.
Removing one test case from the integer regress0.
<folderInfo id="cdt.managedbuild.toolchain.gnu.base.1461790692.1059214216" name="/" resourcePath="">
<toolChain id="cdt.managedbuild.toolchain.gnu.base.1311293674" name="cdt.managedbuild.toolchain.gnu.base" superClass="cdt.managedbuild.toolchain.gnu.base">
<targetPlatform archList="all" binaryParser="org.eclipse.cdt.core.ELF" id="cdt.managedbuild.target.gnu.platform.base.1799734525" name="Debug Platform" osList="linux,hpux,aix,qnx" superClass="cdt.managedbuild.target.gnu.platform.base"/>
- <builder buildPath="${workspace_loc/cvc4/}" id="cdt.managedbuild.target.gnu.builder.base.549477204" incrementalBuildTarget="all" keepEnvironmentInBuildfile="false" managedBuildOn="false" name="Gnu Make Builder" parallelBuildOn="true" parallelizationNumber="2" superClass="cdt.managedbuild.target.gnu.builder.base">
+ <builder buildPath="${workspace_loc/cvc4/}" id="cdt.managedbuild.target.gnu.builder.base.549477204" incrementalBuildTarget="all" keepEnvironmentInBuildfile="false" managedBuildOn="false" name="Gnu Make Builder" parallelBuildOn="true" parallelizationNumber="10" superClass="cdt.managedbuild.target.gnu.builder.base">
<outputEntries>
<entry flags="VALUE_WORKSPACE_PATH|RESOLVED" kind="outputPath" name=""/>
</outputEntries>
<storageModule moduleId="cdtBuildSystem" version="4.0.0">
<project id="cvc4.null.1129006228" name="cvc4"/>
</storageModule>
- <storageModule moduleId="refreshScope"/>
+ <storageModule moduleId="refreshScope" versionNumber="1">
+ <resource resourceType="PROJECT" workspacePath="/cvc4-trunk"/>
+ </storageModule>
<storageModule moduleId="scannerConfiguration">
<autodiscovery enabled="true" problemReportingEnabled="true" selectedProfileId=""/>
<profile id="org.eclipse.cdt.make.core.GCCStandardMakePerProjectProfile">
</dictionary>
<dictionary>
<key>org.eclipse.cdt.make.core.buildArguments</key>
- <value>-j2</value>
+ <value>-j10</value>
</dictionary>
<dictionary>
<key>org.eclipse.cdt.make.core.buildCommand</key>
Debug("minisat") << "got new unit " << ps[0] << " at assertion level " << assertionLevel << std::endl;
trail_user.push(ps[0]);
}
- return ok = (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == CRef_Undef);
+ return ok = (propagate(CHECK_WITHOUTH_THEORY) == CRef_Undef);
} else return ok;
} else {
CRef cr = ca.alloc(assertionLevel, ps, false);
ScopedBool scoped_bool(minisat_busy, true);
- // If we are not in the quick mode add the lemmas that were left begind
- if (type != CHECK_WITHOUTH_PROPAGATION_QUICK && lemmas.size() > 0) {
+ // If we are not in the quick mode add the lemmas that were left behind
+ if (type != CHECK_WITHOUTH_THEORY && lemmas.size() > 0) {
confl = updateLemmas();
if (confl != CRef_Undef) {
return confl;
// If this is the final check, no need for Boolean propagation and
// theory propagation
- if (type == CHECK_WITHOUTH_PROPAGATION_FINAL) {
+ if (type == CHECK_FINAL) {
// Do the theory check
- theoryCheck(CVC4::theory::Theory::FULL_EFFORT);
+ theoryCheck(CVC4::theory::Theory::EFFORT_FULL);
// If there are lemmas (or conflicts) update them
if (lemmas.size() > 0) {
recheck = true;
}
}
- // The effort we will be using to theory check
- CVC4::theory::Theory::Effort effort = type == CHECK_WITHOUTH_PROPAGATION_QUICK ?
- CVC4::theory::Theory::QUICK_CHECK :
- CVC4::theory::Theory::STANDARD;
-
// Keep running until we have checked everything, we
// have no conflict and no new literals have been asserted
- do {
- do {
- // Propagate on the clauses
- confl = propagateBool();
-
- // If no conflict, do the theory check
- if (confl == CRef_Undef) {
- // Do the theory check
- theoryCheck(effort);
- // If there are lemmas (or conflicts) update them
- if (lemmas.size() > 0) {
- confl = updateLemmas();
- }
- }
- } while (confl == CRef_Undef && qhead < trail.size());
-
- // If still consistent do some theory propagation
- if (confl == CRef_Undef && type == CHECK_WITH_PROPAGATION_STANDARD) {
- propagateTheory();
- if (lemmas.size() > 0) {
- confl = updateLemmas();
- }
+ do {
+ // Propagate on the clauses
+ confl = propagateBool();
+
+ // If no conflict, do the theory check
+ if (confl == CRef_Undef && type != CHECK_WITHOUTH_THEORY) {
+ // Do the theory check
+ theoryCheck(CVC4::theory::Theory::EFFORT_STANDARD);
+ // Pick up the theory propagated literals
+ propagateTheory();
+ // If there are lemmas (or conflicts) update them
+ if (lemmas.size() > 0) {
+ confl = updateLemmas();
+ }
}
-
- } while (confl == CRef_Undef && qhead < trail.size());
+ } while (confl == CRef_Undef && qhead < trail.size());
return confl;
}
{
assert(decisionLevel() == 0);
- if (!ok || propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != CRef_Undef)
+ if (!ok || propagate(CHECK_WITHOUTH_THEORY) != CRef_Undef)
return ok = false;
if (nAssigns() == simpDB_assigns || (simpDB_props > 0))
vec<Lit> learnt_clause;
starts++;
- TheoryCheckType check_type = CHECK_WITH_PROPAGATION_STANDARD;
+ TheoryCheckType check_type = CHECK_WITH_THEORY;
for (;;) {
// Propagate and call the theory solvers
}
// We have a conflict so, we are going back to standard checks
- check_type = CHECK_WITH_PROPAGATION_STANDARD;
+ check_type = CHECK_WITH_THEORY;
} else {
// If this was a final check, we are satisfiable
- if (check_type == CHECK_WITHOUTH_PROPAGATION_FINAL) {
+ if (check_type == CHECK_FINAL) {
// Unless a lemma has added more stuff to the queues
if (!order_heap.empty() || qhead < trail.size()) {
- check_type = CHECK_WITH_PROPAGATION_STANDARD;
+ check_type = CHECK_WITH_THEORY;
continue;
} else if (recheck) {
// There some additional stuff added, so we go for another full-check
if (next == lit_Undef) {
// We need to do a full theory check to confirm
- check_type = CHECK_WITHOUTH_PROPAGATION_FINAL;
+ check_type = CHECK_FINAL;
continue;
}
vec<bool> theory; // Is the variable representing a theory atom
enum TheoryCheckType {
- // Quick check, but don't perform theory propagation
- CHECK_WITHOUTH_PROPAGATION_QUICK,
- // Check and perform theory propagation
- CHECK_WITH_PROPAGATION_STANDARD,
- // The SAT problem is satisfiable, perform a full theory check
- CHECK_WITHOUTH_PROPAGATION_FINAL
+ // Quick check, but don't perform theory reasoning
+ CHECK_WITHOUTH_THEORY,
+ // Check and perform theory reasoning
+ CHECK_WITH_THEORY,
+ // The SAT abstraction of the problem is satisfiable, perform a full theory check
+ CHECK_FINAL
};
// Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which it is
updateElimHeap(var(l));
}
- return c.size() == 1 ? enqueue(c[0]) && propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == CRef_Undef : true;
+ return c.size() == 1 ? enqueue(c[0]) && propagate(CHECK_WITHOUTH_THEORY) == CRef_Undef : true;
}
uncheckedEnqueue(~c[i]);
}
- bool result = propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != CRef_Undef;
+ bool result = propagate(CHECK_WITHOUTH_THEORY) != CRef_Undef;
cancelUntil(0);
return result;
}
else
l = c[i];
- if (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != CRef_Undef){
+ if (propagate(CHECK_WITHOUTH_THEORY) != CRef_Undef){
cancelUntil(0);
asymm_lits++;
if (!strengthenClause(cr, l))
}
void TheoryArith::propagate(Effort e) {
- if(quickCheckOrMore(e)){
- bool propagated = false;
- if(Options::current()->arithPropagation && hasAnyUpdates()){
- propagateCandidates();
- }else{
- clearUpdates();
- }
+ bool propagated = false;
+ if(Options::current()->arithPropagation && hasAnyUpdates()){
+ propagateCandidates();
+ }else{
+ clearUpdates();
+ }
- while(d_propManager.hasMorePropagations()){
- const PropManager::PropUnit next = d_propManager.getNextPropagation();
- bool flag = next.flag;
- TNode toProp = next.consequent;
-
- TNode atom = (toProp.getKind() == kind::NOT) ? toProp[0] : toProp;
-
- Debug("arith::propagate") << "propagate @" << getContext()->getLevel() <<" flag: "<< flag << " " << toProp << endl;
-
- if(flag) {
- //Currently if the flag is set this came from an equality detected by the
- //equality engine in the the difference manager.
- if(toProp.getKind() == kind::EQUAL){
- Node normalized = Rewriter::rewrite(toProp);
- Node notNormalized = normalized.notNode();
-
- if(d_diseq.find(notNormalized) == d_diseq.end()){
- d_out->propagate(toProp);
- propagated = true;
- }else{
- Node exp = d_differenceManager.explain(toProp);
- Node lp = flattenAnd(exp.andNode(notNormalized));
- Debug("arith::propagate") << "propagate conflict" << lp << endl;
- d_out->conflict(lp);
-
- propagated = true;
- break;
- }
- }else{
+ while(d_propManager.hasMorePropagations()){
+ const PropManager::PropUnit next = d_propManager.getNextPropagation();
+ bool flag = next.flag;
+ TNode toProp = next.consequent;
+
+ TNode atom = (toProp.getKind() == kind::NOT) ? toProp[0] : toProp;
+
+ Debug("arith::propagate") << "propagate @" << getContext()->getLevel() <<" flag: "<< flag << " " << toProp << endl;
+
+ if(flag) {
+ //Currently if the flag is set this came from an equality detected by the
+ //equality engine in the the difference manager.
+ if(toProp.getKind() == kind::EQUAL){
+ Node normalized = Rewriter::rewrite(toProp);
+ Node notNormalized = normalized.notNode();
+
+ if(d_diseq.find(notNormalized) == d_diseq.end()){
d_out->propagate(toProp);
propagated = true;
+ }else{
+ Node exp = d_differenceManager.explain(toProp);
+ Node lp = flattenAnd(exp.andNode(notNormalized));
+ Debug("arith::propagate") << "propagate conflict" << lp << endl;
+ d_out->conflict(lp);
+
+ propagated = true;
+ break;
}
- }else if(inContextAtom(atom)){
- Node satValue = d_valuation.getSatValue(toProp);
- AlwaysAssert(satValue.isNull());
- propagated = true;
- d_out->propagate(toProp);
}else{
- //Not clear if this is a good time to do this or not...
- Debug("arith::propagate") << "Atom is not in context" << toProp << endl;
-#warning "enable remove atom in database"
- //d_atomDatabase.removeAtom(atom);
+ d_out->propagate(toProp);
+ propagated = true;
}
+ }else if(inContextAtom(atom)){
+ Node satValue = d_valuation.getSatValue(toProp);
+ AlwaysAssert(satValue.isNull());
+ propagated = true;
+ d_out->propagate(toProp);
+ }else{
+ //Not clear if this is a good time to do this or not...
+ Debug("arith::propagate") << "Atom is not in context" << toProp << endl;
+#warning "enable remove atom in database"
+ //d_atomDatabase.removeAtom(atom);
}
+ }
- if(!propagated){
- //Opportunistically export previous conflicts
- while(d_simplex.hasMoreLemmas()){
- Node lemma = d_simplex.popLemma();
- d_out->lemma(lemma);
- }
+ if(!propagated){
+ //Opportunistically export previous conflicts
+ while(d_simplex.hasMoreLemmas()){
+ Node lemma = d_simplex.popLemma();
+ d_out->lemma(lemma);
}
}
}
}
d_learner.clear();
- check(FULL_EFFORT);
+ check(EFFORT_FULL);
}
EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) {
}
}
- if( e == FULL_EFFORT ) {
+ if( e == EFFORT_FULL ) {
Debug("datatypes-split") << "Check for splits " << e << endl;
//do splitting
for( EqLists::iterator i = d_labels.begin(); i != d_labels.end(); i++ ) {
std::ostream& operator<<(std::ostream& os, Theory::Effort level){
switch(level){
- case Theory::MIN_EFFORT:
- os << "MIN_EFFORT"; break;
- case Theory::QUICK_CHECK:
- os << "QUICK_CHECK"; break;
- case Theory::STANDARD:
- os << "STANDARD"; break;
- case Theory::FULL_EFFORT:
- os << "FULL_EFFORT"; break;
+ case Theory::EFFORT_STANDARD:
+ os << "EFFORT_STANDARD"; break;
+ case Theory::EFFORT_FULL:
+ os << "EFFORT_FULL"; break;
+ case Theory::EFFORT_COMBINATION:
+ os << "EFFORT_COMBINATION"; break;
default:
Unreachable();
}
* Returns the ID of the theory responsible for the given node.
*/
static inline TheoryId theoryOf(TNode node) {
- Trace("theory") << "theoryOf(" << node << ")" << std::endl;
+ Trace("theory::internal") << "theoryOf(" << node << ")" << std::endl;
// Constants, variables, 0-ary constructors
if (node.getMetaKind() == kind::metakind::VARIABLE || node.getMetaKind() == kind::metakind::CONSTANT) {
return theoryOf(node.getType());
* with FULL_EFFORT.
*/
enum Effort {
- MIN_EFFORT = 0,
- QUICK_CHECK = 10,
- STANDARD = 50,
- FULL_EFFORT = 100,
- COMBINATION = 150
+ /**
+ * Standard effort where theory need not do anything
+ */
+ EFFORT_STANDARD = 50,
+ /**
+ * Full effort requires the theory make sure its assertions are satisfiable or not
+ */
+ EFFORT_FULL = 100,
+ /**
+ * Combination effort means that the individual theories are already satisfied, and
+ * it is time to put some effort into propagation of shared term equalities
+ */
+ EFFORT_COMBINATION = 150
};/* enum Effort */
- // simple, useful predicates for effort values
- static inline bool minEffortOnly(Effort e) CVC4_CONST_FUNCTION
- { return e == MIN_EFFORT; }
- static inline bool quickCheckOrMore(Effort e) CVC4_CONST_FUNCTION
- { return e >= QUICK_CHECK; }
- static inline bool quickCheckOnly(Effort e) CVC4_CONST_FUNCTION
- { return e >= QUICK_CHECK && e < STANDARD; }
static inline bool standardEffortOrMore(Effort e) CVC4_CONST_FUNCTION
- { return e >= STANDARD; }
+ { return e >= EFFORT_STANDARD; }
static inline bool standardEffortOnly(Effort e) CVC4_CONST_FUNCTION
- { return e >= STANDARD && e < FULL_EFFORT; }
+ { return e >= EFFORT_STANDARD && e < EFFORT_FULL; }
static inline bool fullEffort(Effort e) CVC4_CONST_FUNCTION
- { return e == FULL_EFFORT; }
+ { return e == EFFORT_FULL; }
static inline bool combination(Effort e) CVC4_CONST_FUNCTION
- { return e == COMBINATION; }
+ { return e == EFFORT_COMBINATION; }
/**
* Get the id for this Theory.
* - throw an exception
* - or call get() until done() is true.
*/
- virtual void check(Effort level = FULL_EFFORT) { }
+ virtual void check(Effort level = EFFORT_FULL) { }
/**
* T-propagate new literal assignments in the current context.
*/
- virtual void propagate(Effort level = FULL_EFFORT) { }
+ virtual void propagate(Effort level = EFFORT_FULL) { }
/**
* Return an explanation for the literal represented by parameter n
arith-int-013.cvc \
arith-int-022.cvc \
arith-int-024.cvc \
- arith-int-041.cvc \
arith-int-042.cvc \
arith-int-042.min.cvc \
arith-int-047.cvc \
arith-int-038.cvc \
arith-int-039.cvc \
arith-int-040.cvc \
+ arith-int-041.cvc \
arith-int-043.cvc \
arith-int-044.cvc \
arith-int-045.cvc \
public:
- TheoryArithWhite() : d_level(Theory::FULL_EFFORT), d_zero(0), d_one(1), debug(false) {}
+ TheoryArithWhite() : d_level(Theory::EFFORT_FULL), d_zero(0), d_one(1), debug(false) {}
void fakeTheoryEnginePreprocess(TNode inp){
Node rewrite = inp; //FIXME this needs to enforce that inp is fully rewritten already!
}
void testEffort(){
- Theory::Effort m = Theory::MIN_EFFORT;
- Theory::Effort q = Theory::QUICK_CHECK;
- Theory::Effort s = Theory::STANDARD;
- Theory::Effort f = Theory::FULL_EFFORT;
-
- TS_ASSERT( Theory::minEffortOnly(m));
- TS_ASSERT(!Theory::minEffortOnly(q));
- TS_ASSERT(!Theory::minEffortOnly(s));
- TS_ASSERT(!Theory::minEffortOnly(f));
-
- TS_ASSERT(!Theory::quickCheckOnly(m));
- TS_ASSERT( Theory::quickCheckOnly(q));
- TS_ASSERT(!Theory::quickCheckOnly(s));
- TS_ASSERT(!Theory::quickCheckOnly(f));
-
- TS_ASSERT(!Theory::standardEffortOnly(m));
- TS_ASSERT(!Theory::standardEffortOnly(q));
+ Theory::Effort s = Theory::EFFORT_STANDARD;
+ Theory::Effort f = Theory::EFFORT_FULL;
+
TS_ASSERT( Theory::standardEffortOnly(s));
TS_ASSERT(!Theory::standardEffortOnly(f));
- TS_ASSERT(!Theory::fullEffort(m));
- TS_ASSERT(!Theory::fullEffort(q));
TS_ASSERT(!Theory::fullEffort(s));
TS_ASSERT( Theory::fullEffort(f));
- TS_ASSERT(!Theory::quickCheckOrMore(m));
- TS_ASSERT( Theory::quickCheckOrMore(q));
- TS_ASSERT( Theory::quickCheckOrMore(s));
- TS_ASSERT( Theory::quickCheckOrMore(f));
-
- TS_ASSERT(!Theory::standardEffortOrMore(m));
- TS_ASSERT(!Theory::standardEffortOrMore(q));
TS_ASSERT( Theory::standardEffortOrMore(s));
TS_ASSERT( Theory::standardEffortOrMore(f));
}
TS_ASSERT(!d_dummy->doneWrapper());
- d_dummy->check(Theory::FULL_EFFORT);
+ d_dummy->check(Theory::EFFORT_FULL);
TS_ASSERT(d_dummy->doneWrapper());
}
projects / cvc5.git / commitdiff