When proof enabled, disable uf sym break. Add regression.

diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index b546fcf87c2cd7d9b42acf9407836d9385445d85..263e1fe8cb37d2cbea92740c9379bfa249a84738 100644 (file)
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -87,6 +87,7 @@ void LFSCCnfProof::printPreprocess(std::ostream& os, std::ostream& paren) {
       os << "(th_let_pf _ ";
 
       //TODO
+      Trace("cnf-pf-debug") << "; preprocess assertion : " << e << std::endl;
       os << "(trust_f ";
       LFSCTheoryProof::printTerm(e, os);
       os << ") ";
@@ -132,7 +133,9 @@ void LFSCCnfProof::printInputClauses(std::ostream& os, std::ostream& paren) {
 
     Expr base_assertion = ProofManager::currentPM()->getFormulaForClauseId( id );
     ProofRule pr = ProofManager::currentPM()->getProofRuleForClauseId( id );
-
+    Trace("cnf-pf") << std::endl;
+    Trace("cnf-pf") << "; formula for clause id " << id << " : " << base_assertion << std::endl;
+    
     //get the assertion for the clause id
     std::map< Expr, unsigned > childIndex;
     std::map< Expr, bool > childPol;
@@ -152,7 +155,6 @@ void LFSCCnfProof::printInputClauses(std::ostream& os, std::ostream& paren) {
     std::map< Expr, unsigned >::iterator itci = childIndex.find( base_assertion );
     bool is_in_clause = itci!=childIndex.end();
     unsigned base_index = is_in_clause ? itci->second : 0;
-    Trace("cnf-pf") << std::endl;
     Trace("cnf-pf") << "; input = " << is_input << ", is_in_clause = " << is_in_clause << ", id = " << id << ", assertion = " << assertion << ", base assertion = " << base_assertion << std::endl;
     if( !is_input ){
       Assert( is_in_clause );

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 2d8c4178a5c07fecd69345ec0ea80cd78caa2e09..311d4afeb4f0d0f52ea39b779bdc4917afec5150 100644 (file)
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -176,15 +176,16 @@ void ProofManager::addClause(ClauseId id, const prop::SatClause* clause, ClauseK
     d_propVars.insert(lit.getSatVariable());
   }*/
   if (kind == INPUT) {
+    Debug("cores") << "; Add to inputClauses " << id << std::endl;
     d_inputClauses.insert(std::make_pair(id, clause));
     Assert(d_satProof->d_inputClauses.find(id) != d_satProof->d_inputClauses.end());
-    Debug("cores") << "core id is " << d_satProof->d_inputClauses[id] << std::endl;
+    Debug("cores") << "; core id is " << d_satProof->d_inputClauses[id] << std::endl;
     if(d_satProof->d_inputClauses[id] == uint64_t(-1)) {
-      Debug("cores") << " + constant unit (true or false)" << std::endl;
+      Debug("cores") << "; + constant unit (true or false)" << std::endl;
     } else if(options::unsatCores()) {
       Expr e = d_cnfProof->getAssertion(d_satProof->d_inputClauses[id] & 0xffffffff);
-      Debug("cores") << "core input assertion from CnfStream is " << e << std::endl;
-      Debug("cores") << "with proof rule " << ((d_satProof->d_inputClauses[id] & 0xffffffff00000000llu) >> 32) << std::endl;
+      Debug("cores") << "; core input assertion from CnfStream is " << e << std::endl;
+      Debug("cores") << "; with proof rule " << ((d_satProof->d_inputClauses[id] & 0xffffffff00000000llu) >> 32) << std::endl;
       // Invalid proof rules are currently used for parts of CVC4 that don't
       // support proofs (these are e.g. unproven theory lemmas) or don't need
       // proofs (e.g. split lemmas).  We can ignore these safely when
@@ -331,12 +332,13 @@ bool ProofManager::isInputAssertion( Expr e, std::ostream& out ) {
 }
 
 void ProofManager::setRegisteringFormula( Node n, ProofRule proof_id ) {
+  Trace("cnf-pf-debug") << "; set registering formula " << n << " proof rule = " << proof_id << std::endl;
   d_registering_assertion = n;
   d_registering_rule = proof_id;
 }
 
 void ProofManager::setRegisteredClauseId( ClauseId id ) {
-  Trace("cnf-pf-debug") << "set register clause id " << id << " " << d_registering_assertion << std::endl;
+  Trace("cnf-pf-debug") << "; set register clause id " << id << " " << d_registering_assertion << std::endl;
   if( !d_registering_assertion.isNull() ){
      d_clause_id_to_assertion[id] = d_registering_assertion.toExpr();
      d_clause_id_to_rule[id] = d_registering_rule;

diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp
index 7867f1ddcff4fcf979c22e94417a6648efad195f..6854f4940bc9b4e9889002fc48a7fe7751fd50eb 100644 (file)
--- a/src/proof/sat_proof.cpp
+++ b/src/proof/sat_proof.cpp
@@ -364,12 +364,12 @@ void SatProof::printRes(ResChain* res) {
 /// registration methods
 
 ClauseId SatProof::registerClause(Minisat::CRef clause, ClauseKind kind, uint64_t proof_id) {
-  Debug("cores") << "registerClause " << proof_id << std::endl;
+  Debug("cores") << "registerClause, proof id = " << proof_id << std::endl;
   Assert(clause != CRef_Undef);
   ClauseIdMap::iterator it = d_clauseId.find(clause);
   if (it == d_clauseId.end()) {
     ClauseId newId = ProofManager::currentPM()->nextId();
-    d_clauseId.insert(ClauseIdMap::value_type(clause, newId)); 
+    d_clauseId.insert(ClauseIdMap::value_type(clause, newId));
     d_idClause.insert(IdCRefMap::value_type(newId, clause));
     if (kind == INPUT) {
       Assert(d_inputClauses.find(newId) == d_inputClauses.end());

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index f03cc994404f6dfb2cf7e63272426caf35ef0821..b0b135b04db51dd091589e08102260cf61d726b4 100644 (file)
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -667,7 +667,7 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated
     Assert((uint64_t(proof_id) & 0xffffffff00000000llu) == 0 && (assertionTableIndex & 0xffffffff00000000llu) == 0, "proof_id/table_index collision");
     d_proofId = assertionTableIndex | (uint64_t(proof_id) << 32);
     d_assertionTable.push_back(from.isNull() ? node : from);
-    Debug("cores") << "cnf ix " << assertionTableIndex << " asst " << node << "  proof_id " << proof_id << " from " << from << endl;
+    Debug("cores") << "; cnf is " << assertionTableIndex << " asst " << node << "  proof_id " << proof_id << " from " << from << endl;
   } else {
     // We aren't producing proofs or unsat cores; use an invalid proof id.
     d_proofId = uint64_t(-1);

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 11a412c7529a6a5755f77b23d61a6665a463d02d..9fe3a115de30ca4cf57388c8eef1a46a94b5d9e5 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -700,9 +700,9 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   d_modelGlobalCommands(),
   d_modelCommands(NULL),
   d_dumpCommands(),
-#ifdef CVC4_PROOF  
+#ifdef CVC4_PROOF
   d_defineCommands(),
-#endif  
+#endif
   d_logic(),
   d_originalOptions(em->getOptions()),
   d_pendingPops(0),
@@ -1083,7 +1083,7 @@ void SmtEngine::setDefaults() {
 
   // by default, symmetry breaker is on only for QF_UF
   if(! options::ufSymmetryBreaker.wasSetByUser()) {
-    bool qf_uf = d_logic.isPure(THEORY_UF) && !d_logic.isQuantified();
+    bool qf_uf = d_logic.isPure(THEORY_UF) && !d_logic.isQuantified() && !options::proof();
     Trace("smt") << "setting uf symmetry breaker to " << qf_uf << endl;
     options::ufSymmetryBreaker.set(qf_uf);
   }
@@ -1168,8 +1168,8 @@ void SmtEngine::setDefaults() {
   if(! options::repeatSimp.wasSetByUser()) {
     bool repeatSimp = !d_logic.isQuantified() &&
                       (d_logic.isTheoryEnabled(THEORY_ARRAY) &&
-                      d_logic.isTheoryEnabled(THEORY_UF) &&
-                      d_logic.isTheoryEnabled(THEORY_BV)) &&
+                      d_logic.isTheoryEnabled(THEORY_UF) &&
+                      d_logic.isTheoryEnabled(THEORY_BV)) &&
                       !options::unsatCores();
     Trace("smt") << "setting repeat simplification to " << repeatSimp << endl;
     options::repeatSimp.set(repeatSimp);
@@ -1713,7 +1713,7 @@ void SmtEngine::defineFunction(Expr func,
       d_defineCommands.push_back(c.clone());
     });
 
-  
+
   // Substitute out any abstract values in formula
   Expr form = d_private->substituteAbstractValues(Node::fromExpr(formula)).toExpr();
 
@@ -3087,7 +3087,7 @@ void SmtEnginePrivate::processAssertions() {
   Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl;
 
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
-  
+
   if (d_assertions.size() == 0) {
     // nothing to do
     return;
@@ -3385,7 +3385,7 @@ void SmtEnginePrivate::processAssertions() {
           d_iteSkolemMap.erase(toErase.back());
           toErase.pop_back();
         }
-       d_assertions[d_realAssertionsEnd - 1] = Rewriter::rewrite(Node(builder));
+        d_assertions[d_realAssertionsEnd - 1] = Rewriter::rewrite(Node(builder));
       }
       // For some reason this is needed for some benchmarks, such as
       // http://cvc4.cs.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2
@@ -3497,7 +3497,7 @@ void SmtEnginePrivate::addFormula(TNode n, bool inUnsatCore, bool inInput)
     }
     // rewrite rules are by default in the unsat core because
     // they need to be applied until saturation
-    if(options::unsatCores() && 
+    if(options::unsatCores() &&
        n.getKind() == kind::REWRITE_RULE ){
       ProofManager::currentPM()->addUnsatCore(n.toExpr());
     }
@@ -4030,8 +4030,8 @@ void SmtEngine::checkUnsatCore() {
   for (; itg != d_defineCommands.end();  ++itg) {
     (*itg)->invoke(&coreChecker);
   }
-       );
-  
+  );
+
   Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions (size == " << core.size() << ")" << endl;
   for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
     Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i << endl;

diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am
index 50de00b61736f312ec6402d5dc8b743459d16ac5..c9a47c26f06b47b0feb46f57751a0d147c118da8 100644 (file)
--- a/test/regress/regress0/uf/Makefile.am
+++ b/test/regress/regress0/uf/Makefile.am
@@ -49,7 +49,8 @@ TESTS =       \
        cnf-iff.smt2 \
        cnf-iff-base.smt2 \
        cnf-ite.smt2 \
-       cnf-and-neg.smt2
+       cnf-and-neg.smt2 \
+       cnf_abc.smt2
 
 EXTRA_DIST = $(TESTS) \
        mkpidgeon

diff --git a/test/regress/regress0/uf/cnf_abc.smt2 b/test/regress/regress0/uf/cnf_abc.smt2
new file mode 100755 (executable)
index 0000000..5d011f4
--- /dev/null
+++ b/test/regress/regress0/uf/cnf_abc.smt2
@@ -0,0 +1,168 @@
+(set-logic QF_UF)\r
+(set-info :status unsat)\r
+\r
+(declare-sort I 0)\r
+(declare-fun f (I I) I)\r
+(declare-fun a () I)\r
+(declare-fun b () I)\r
+(declare-fun c () I)\r
+\r
+\r
+\r
+(assert\r
+ (or\r
+  (= (f a a) a)\r
+  (= (f a a) b)\r
+  (= (f a a) c)\r
+  ))\r
+\r
+(assert\r
+ (or\r
+  (= (f a b) a)\r
+  (= (f a b) b)\r
+  (= (f a b) c)\r
+  ))\r
+\r
+(assert\r
+ (or\r
+  (= (f a c) a)\r
+  (= (f a c) b)\r
+  (= (f a c) c)\r
+  ))\r
+\r
+(assert\r
+ (or\r
+  (= (f b a) a)\r
+  (= (f b a) b)\r
+  (= (f b a) c)\r
+  ))\r
+\r
+(assert\r
+ (or\r
+  (= (f b b) a)\r
+  (= (f b b) b)\r
+  (= (f b b) c)\r
+  ))\r
+\r
+(assert\r
+ (or\r
+  (= (f b c) a)\r
+  (= (f b c) b)\r
+  (= (f b c) c)\r
+  ))\r
+\r
+\r
+(assert\r
+ (or\r
+  (= (f c a) a)\r
+  (= (f c a) b)\r
+  (= (f c a) c)\r
+  ))\r
+\r
+(assert\r
+ (or\r
+  (= (f c b) a)\r
+  (= (f c b) b)\r
+  (= (f c b) c)\r
+  ))\r
+\r
+(assert\r
+ (or\r
+  (= (f c c) a)\r
+  (= (f c c) b)\r
+  (= (f c c) c)\r
+  ))\r
+\r
+\r
+\r
+(assert\r
+ (or\r
+  (= (f a a) a)\r
+  (= (f b b) a)\r
+  (= (f c c) a)\r
+  ))\r
+\r
+(assert\r
+ (or\r
+  (= (f a a) b)\r
+  (= (f b b) b)\r
+  (= (f c c) b)\r
+  ))\r
+\r
+(assert\r
+ (or\r
+  (= (f a a) c)\r
+  (= (f b b) c)\r
+  (= (f c c) c)\r
+  ))\r
+\r
+\r
+\r
+(assert\r
+ (or\r
+  (= (f a a) a)\r
+  (= (f b a) b)\r
+  (= (f c a) c)\r
+  ))\r
+\r
+(assert\r
+ (or\r
+  (= (f a b) a)\r
+  (= (f b b) b)\r
+  (= (f c b) c)\r
+  ))\r
+\r
+(assert\r
+ (or\r
+  (= (f a c) a)\r
+  (= (f b c) b)\r
+  (= (f c c) c)\r
+  ))\r
+\r
+\r
+\r
+\r
+(assert (not (= (f a a) a)))\r
+(assert (not (= (f b b) b)))\r
+(assert (not (= (f c c) c)))                \r
+\r
+\r
+(assert\r
+ (or\r
+  (not (= (f a (f a a)) a))\r
+  (not (= (f a (f a b)) b))\r
+  (not (= (f a (f a c)) c))\r
+  ))\r
+\r
+(assert\r
+ (or\r
+  (not (= (f b (f b a)) a)) \r
+  (not (= (f b (f b b)) b))\r
+  (not (= (f b (f b c)) c))\r
+  ))\r
+\r
+(assert\r
+ (or\r
+  (not (= (f c (f c a)) a)) \r
+  (not (= (f c (f c b)) b))\r
+  (not (= (f c (f c c)) c))\r
+  ))\r
+\r
+\r
+(assert  (not (= (f a a) (f b a))))\r
+(assert  (not (= (f a a) (f c a))))\r
+(assert  (not (= (f b a) (f c a))))\r
+\r
+(assert  (not (= (f a b) (f b b))))\r
+(assert  (not (= (f a b) (f c b))))\r
+(assert  (not (= (f b b) (f c b))))\r
+\r
+(assert  (not (= (f a c) (f b c))))\r
+(assert  (not (= (f a c) (f c c))))\r
+(assert  (not (= (f b c) (f c c))))\r
+\r
+\r
+\r
+(check-sat)\r
+\r
+(exit)\r