add CMS xor extension to dimacs front-end

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/sat/dimacs.cpp

@@ -126,6 +126,13 @@ static bool parse_dimacs_core(Buffer & in, std::ostream& err, sat::solver & solv
             else if (*in == 'c' || *in == 'p') {
                 skip_line(in);
             }
+            else if (*in == 'x') {
+                ++in;
+                read_clause(in, err, solver, lits);
+                if (!solver.get_extension())
+                    throw default_exception("you have to set sat.xor.enable=true to use the CMS xor extension");
+                solver.mk_xor_clause(lits);
+            }
             else {
                 read_clause(in, err, solver, lits);
                 solver.mk_clause(lits.size(), lits.data());
@@ -227,7 +234,6 @@ namespace dimacs {
     }
 
     bool drat_parser::next() {
-        int theory_id;
         try {
         loop:
             skip_whitespace(in);
@@ -240,38 +246,13 @@ namespace dimacs {
                 // parse meta-data information
                 skip_line(in);
                 goto loop;
-            case 'i':
-                // parse input clause
-                ++in;
-                skip_whitespace(in);
-                read_clause(in, err, m_record.m_lits);
-                m_record.m_status = sat::status::input();
-                break;
-            case 'a':
-                // parse non-redundant theory clause
-                ++in;
-                skip_whitespace(in);
-                theory_id = read_theory_id();
-                skip_whitespace(in);
-                read_clause(in, err, m_record.m_lits);
-                m_record.m_status = sat::status::th(false, theory_id);
-                break;
             case 'd':
                 // parse clause deletion
                 ++in;
                 skip_whitespace(in);
                 read_clause(in, err, m_record.m_lits);
                 m_record.m_status = sat::status::deleted();
-                break;
-            case 'r':
-                // parse redundant theory clause
-                // the clause must be DRUP redundant modulo T
-                ++in;
-                skip_whitespace(in);
-                theory_id = read_theory_id();
-                read_clause(in, err, m_record.m_lits);
-                m_record.m_status = sat::status::th(true, theory_id);
-                break;
+                break;                
             default:
                 // parse clause redundant modulo DRAT (or mostly just DRUP)
                 read_clause(in, err, m_record.m_lits);

src/sat/sat_solver.cpp

@@ -339,6 +339,12 @@ namespace sat {
     }
 
 
+    void solver::mk_xor_clause(sat::literal_vector const& lits) {
+        SASSERT(m_ext);
+        m_ext->add_xor(lits);
+    }
+
+
     clause* solver::mk_clause(unsigned num_lits, literal * lits, sat::status st) {
         m_model_is_current = false;
             

src/sat/sat_solver.h

@@ -282,6 +282,8 @@ namespace sat {
         clause* mk_clause(literal l1, literal l2, sat::status st = sat::status::asserted());
         clause* mk_clause(literal l1, literal l2, literal l3, sat::status st = sat::status::asserted());
 
+        void mk_xor_clause(sat::literal_vector const& lits);
+
         random_gen& rand() { return m_rand; }
 
         void set_trim() { m_trim = true; }

src/sat/smt/xor_solver.cpp

@@ -21,13 +21,12 @@ namespace xr {
 
 
     solver::solver(euf::solver& ctx):
-        solver(ctx.get_manager(), ctx.get_si(), ctx.get_manager().get_family_id("xor")) {
+        solver(ctx.get_manager(), ctx.get_manager().mk_family_id("xor")) {
         m_ctx = &ctx;
     }
 
-    solver::solver(ast_manager& m, sat::sat_internalizer& si, euf::theory_id id)
-        : euf::th_solver(m, symbol("xor"), id),
-          si(si) {
+    solver::solver(ast_manager& m, euf::theory_id id)
+        : euf::th_solver(m, symbol("xor"), id) {
     }
 
     euf::th_solver* solver::clone(euf::solver& ctx) {

src/sat/smt/xor_solver.h

@@ -166,7 +166,6 @@ namespace xr {
 
 
         euf::solver* m_ctx = nullptr;
-        sat::sat_internalizer& si;
 
         ptr_vector<constraint> m_constraints;
 
@@ -174,7 +173,7 @@ namespace xr {
 
     public:
         solver(euf::solver& ctx);
-        solver(ast_manager& m, sat::sat_internalizer& si, euf::theory_id id);
+        solver(ast_manager& m, euf::theory_id id);
         th_solver* clone(euf::solver& ctx) override;
 
 

src/sat/tactic/goal2sat.cpp

@@ -751,7 +751,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
         sat::extension* ext = m_solver.get_extension();
         if (ext)
             return;
-        auto* x = alloc(xr::solver, m, *this, m.get_family_id("xor"));
+        auto* x = alloc(xr::solver, m, m.get_family_id("xor"));
         m_solver.set_extension(x);        
     }
 

src/shell/dimacs_frontend.cpp

@@ -27,6 +27,7 @@ Revision History:
 #include "sat/sat_solver.h"
 #include "sat/tactic/goal2sat.h"
 #include "sat/tactic/sat2goal.h"
+#include "sat/smt/xor_solver.h"
 #include "ast/reg_decl_plugins.h"
 #include "tactic/tactic.h"
 #include "tactic/fd_solver/fd_solver.h"
@@ -230,6 +231,15 @@ unsigned read_dimacs(char const * file_name) {
     sat_params sp(p);
     reslimit limit;
     sat::solver solver(p, limit);
+
+    // the xor solver uses ast_manager to be compatible with the th_solver API.
+    // we allocate an ast manager on demand if xor is enabled.
+    scoped_ptr<ast_manager> mp;
+    if (sp.xor_enable()) {
+        mp = alloc(ast_manager);
+        reg_decl_plugins(*mp);    
+        solver.set_extension(alloc(xr::solver, *mp, mp->mk_family_id("xor")));
+    }
     g_solver = &solver;
 
     if (file_name) {