Implemented SMT-LIB2 'get-proof'

usi-verification-and-security · Mar 25, 2024 · 84f1c2b · 84f1c2b
1 parent 327eeb7
commit 84f1c2b
Show file tree

Hide file tree

Showing 6 changed files with 36 additions and 6 deletions.
diff --git a/src/api/Interpret.cc b/src/api/Interpret.cc
@@ -267,6 +267,19 @@ void Interpret::interp(ASTNode& n) {
                 }
                 break;
             }
+            case t_getproof: {
+                if (config.produce_proof()) {
+                    if (isInitialized()) {
+                        getProof();
+                    } else {
+                        notify_formatted(true, "Illegal command before set-logic: get-proof");
+                    }
+                } else {
+                    notify_formatted(true,
+                                     "Option to produce proofs has not been set, skipping this command ...");
+                }
+                break;
+            }
             case t_getinterpolants: {
                 if (config.produce_inter()) {
                     if (isInitialized()) {
@@ -1260,6 +1273,11 @@ SRef Interpret::sortFromASTNode(ASTNode const & node) const {
     return logic->getSort(symRef, std::move(args));
 }
 
+void Interpret::getProof()
+{
+    main_solver->printResolutionProofSMT2();
+}
+
 void Interpret::getInterpolants(const ASTNode& n)
 {
     auto exps = *n.children;

diff --git a/src/api/Interpret.h b/src/api/Interpret.h
@@ -170,6 +170,7 @@ class Interpret {
     bool                        storeDefinedFun(std::string const & fname, const vec<PTRef>& args, SRef ret_sort, const PTRef tr);
 
     virtual void                exit();
+    void                        getProof();
     void                        getInterpolants(const ASTNode& n);
     void                        interp (ASTNode& n);
 

diff --git a/src/api/MainSolver.cc b/src/api/MainSolver.cc
@@ -223,6 +223,14 @@ std::unique_ptr<Model> MainSolver::getModel() {
     return modelBuilder.build();
 }
 
+void MainSolver::printResolutionProofSMT2() const {
+    assert(smt_solver);
+    if (!smt_solver->logsResolutionProof()) { throw OsmtApiException("Proofs are not tracked"); }
+    if (status != s_False) { throw OsmtApiException("Proof cannot be created if solver is not in UNSAT state"); }
+
+    return smt_solver->printResolutionProofSMT2(std::cout);
+}
+
 lbool MainSolver::getTermValue(PTRef tr) const {
     if (logic.getSortRef(tr) != logic.getSort_bool()) { return l_Undef; }
     if (not term_mapper->hasLit(tr)) { return l_Undef; }

diff --git a/src/api/MainSolver.h b/src/api/MainSolver.h
@@ -236,6 +236,9 @@ class MainSolver {
     // Returns model of the last query (must be in satisfiable state)
     std::unique_ptr<Model> getModel();
 
+    // Prints proof of the last query (must be in unsatisfiable state)
+    void printResolutionProofSMT2() const;
+
     void stop() { smt_solver->stop = true; }
 
     // Returns interpolation context for the last query (must be in UNSAT state)

diff --git a/src/smtsolvers/ResolutionProof.cc b/src/smtsolvers/ResolutionProof.cc
@@ -134,7 +134,7 @@ bool ResolutionProof::deleted(CRef cr)
   return true;
 }
 
-void ResolutionProof::printSMT2(std::ostream & out, CoreSMTSolver & s, THandler & t)
+void ResolutionProof::printSMT2(std::ostream & out, CoreSMTSolver & s, THandler & t) const
 {
   if ( clause_to_proof_der.find( CRef_Undef ) == clause_to_proof_der.end( ) )
     throw OsmtInternalException("there is no proof of false");
@@ -158,7 +158,7 @@ void ResolutionProof::printSMT2(std::ostream & out, CoreSMTSolver & s, THandler
       continue;
     }
     assert( clause_to_proof_der.find( cr ) != clause_to_proof_der.end( ) );
-    ResolutionProofDer * d = &clause_to_proof_der.at(cr);
+    ResolutionProofDer const * d = &clause_to_proof_der.at(cr);
 
     // Special case in which there is not
     // a derivation but just an equivalence
@@ -170,7 +170,7 @@ void ResolutionProof::printSMT2(std::ostream & out, CoreSMTSolver & s, THandler
       cr = d->chain_cla[0];
       // Retrieve derivation
       assert( clause_to_proof_der.find( cr ) != clause_to_proof_der.end( ) );
-      d = &clause_to_proof_der[ cr ];
+      d = &clause_to_proof_der.at(cr);
     }
     assert( d->chain_cla.size( ) != 1 );
     // Look for unprocessed children
@@ -201,8 +201,8 @@ void ResolutionProof::printSMT2(std::ostream & out, CoreSMTSolver & s, THandler
       out << "(let (cls_" << cr;
       nof_lets ++;
 
-      std::vector< CRef > & chain_cla = d->chain_cla;
-      std::vector< Var > & chain_var = d->chain_var;
+      auto & chain_cla = d->chain_cla;
+      auto & chain_var = d->chain_var;
 
       assert( chain_cla.size( ) == chain_var.size( ) + 1 );
 

diff --git a/src/smtsolvers/ResolutionProof.h b/src/smtsolvers/ResolutionProof.h
@@ -152,7 +152,7 @@ class ResolutionProof
     bool deleted(CRef);                             // Remove clauses if possible
     inline Clause& getClause(CRef cr) const { return cl_al[cr]; } // Get clause from reference
 
-    void printSMT2(std::ostream &, CoreSMTSolver &, THandler &);     // Print proof in SMT-LIB format
+    void printSMT2(std::ostream &, CoreSMTSolver &, THandler &) const;     // Print proof in SMT-LIB format
 
     std::vector<Lit> getAssumedLiterals() const {
         std::vector<Lit> res;