feat(opensmt/smtsolver/CoreSMTSolver): short SAT functionality

close dreal#96
danbryce · May 4, 2015 · f78ce65 · f78ce65
1 parent 7c51e81
commit f78ce65
Show file tree

Hide file tree

Showing 2 changed files with 37 additions and 3 deletions.
diff --git a/src/opensmt/smtsolvers/CoreSMTSolver.C b/src/opensmt/smtsolvers/CoreSMTSolver.C
@@ -1711,9 +1711,16 @@ lbool CoreSMTSolver::search(int nof_conflicts, int nof_learnts)
         }
 
         if (next == lit_Undef){
-          // New variable decision:
-          decisions++;
-          next = pickBranchLit(polarity_mode, random_var_freq);
+          if ((!config.nra_short_sat) || (!entailment())) {
+        	// New variable decision:
+        		DREAL_LOG_INFO << "Pick branch on a lit: " << endl;
+        		decisions++;
+        		next = pickBranchLit(polarity_mode, random_var_freq);
+        	} else {
+        		// SAT formula is satisfiable
+        		next = lit_Undef;
+        		DREAL_LOG_INFO << "Found Model after # decisions " << decisions << endl;
+        	}
 
           // Complete Call
           if ( next == lit_Undef )
@@ -1742,6 +1749,11 @@ lbool CoreSMTSolver::search(int nof_conflicts, int nof_learnts)
             if ( res == 2 ) { continue; }
             if ( res == -1 ) return l_False;
             assert( res == 1 );
+
+            if(config.nra_short_sat) {
+            	// the problem is satisfiable as res = 1 at this point
+            	return l_True;
+            }
             // Otherwise we still have to make sure that
             // splitting on demand did not add any new variable
             decisions++;
@@ -1950,6 +1962,27 @@ int CoreSMTSolver::restartNextLimit ( int nof_conflicts )
   // Standard restart
   return nof_conflicts * restart_inc;
 }
+/*_________________________________________________________________________________________________
+ |
+ |  entailment : ()  ->  [lbool]
+ |
+ |  Description:
+ |   Checks if all clauses are satisfied.
+ |
+ |  Output:
+ |    'l_True' if all clauses are satisfied. 'l_False'
+ |    if there exists unsatisfied clause.
+ |________________________________________________________________________________________________@*/
+
+bool CoreSMTSolver::entailment() {
+  for (int c = 0; c < nClauses(); c++) {
+    if (!satisfied(*clauses[c])) {
+      return false;
+    }
+  }
+
+  return true;
+}
 
 #ifdef STATISTICS
 void CoreSMTSolver::printStatistics( ostream & os )

diff --git a/src/opensmt/smtsolvers/CoreSMTSolver.h b/src/opensmt/smtsolvers/CoreSMTSolver.h
@@ -335,6 +335,7 @@ class CoreSMTSolver : public SMTSolver
         int    restartNextLimit       ( int );         // Next conflict limit for restart
         Var    generateMoreEij        ( );             // Generate more eij
         Var    generateNextEij        ( );             // Generate next eij
+        bool   entailment             ( );             // Check is a partial assignment entails a formula
 
 #ifndef SMTCOMP
         void   dumpCNF                ( );             // Dumps CNF to cnf.smt2