From: Ying Sheng Date: Mon, 16 Dec 2019 19:42:36 +0000 (-0800) Subject: Support ackermannization on uninterpreted sorts in BV (#3372) X-Git-Tag: cvc5-1.0.0~3758 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=49f0f09c6ef1c04fcd5b088456cea9998cff3c91;p=cvc5.git Support ackermannization on uninterpreted sorts in BV (#3372) Support ackermannization on uninterpreted sorts in BV. For uninterpreted sorts, we create a bit-vector sort to replace it. For an uninterpreted sort `S`, if the number of variables within sort `S` is `n`, the replacing bit-vector will have size (log n)+1. --- diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp index 87c7fa2ce..888456174 100644 --- a/src/preprocessing/passes/ackermann.cpp +++ b/src/preprocessing/passes/ackermann.cpp @@ -22,8 +22,9 @@ **/ #include "preprocessing/passes/ackermann.h" - +#include #include "base/check.h" +#include "expr/node_algorithm.h" #include "options/options.h" using namespace CVC4; @@ -186,9 +187,111 @@ void collectFunctionsAndLemmas(FunctionToArgsMap& fun_to_args, /* -------------------------------------------------------------------------- */ +/* Given a minimum capacity for an uninterpreted sort, return the size of the + * new BV type */ +size_t getBVSkolemSize(size_t capacity) +{ + return static_cast(log2(capacity)) + 1; +} + +/* Given the lowest capacity requirements for each uninterpreted sort, assign + * a sufficient bit-vector size. + * Populate usVarsToBVVars so that it maps variables with uninterpreted sort to + * the fresh skolem BV variables. variables */ +void collectUSortsToBV(const unordered_set& vars, + const USortToBVSizeMap& usortCardinality, + SubstitutionMap& usVarsToBVVars) +{ + NodeManager* nm = NodeManager::currentNM(); + + for (TNode var : vars) + { + TypeNode type = var.getType(); + size_t size = getBVSkolemSize(usortCardinality.at(type)); + Node skolem = nm->mkSkolem( + "BVSKOLEM$$", + nm->mkBitVectorType(size), + "a variable created by the ackermannization " + "preprocessing pass, representing a variable with uninterpreted sort " + + type.toString() + "."); + usVarsToBVVars.addSubstitution(var, skolem); + } +} + +/* This function returns the list of terms with uninterpreted sort in the + * formula represented by assertions. */ +std::unordered_set getVarsWithUSorts( + AssertionPipeline* assertions) +{ + std::unordered_set res; + + for (const Node& assertion : assertions->ref()) + { + std::unordered_set vars; + expr::getVariables(assertion, vars); + + for (const TNode& var : vars) + { + if (var.getType().isSort()) + { + res.insert(var); + } + } + } + + return res; +} + +/* This is the top level of converting uninterpreted sorts to bit-vectors. + * We count the number of different variables for each uninterpreted sort. + * Then for each sort, we will assign a new bit-vector type with a sufficient + * size. The size is calculated to have enough capacity, that can accommodate + * the variables occured in the original formula. At the end, all variables of + * uninterpreted sorts will be converted into Skolem variables of BV */ +void usortsToBitVectors(const LogicInfo& d_logic, + AssertionPipeline* assertions, + USortToBVSizeMap& usortCardinality, + SubstitutionMap& usVarsToBVVars) +{ + std::unordered_set toProcess = + getVarsWithUSorts(assertions); + + if (toProcess.size() > 0) + { + /* the current version only supports BV for removing uninterpreted sorts */ + if (not d_logic.isTheoryEnabled(theory::THEORY_BV)) + { + return; + } + + for (TNode term : toProcess) + { + TypeNode type = term.getType(); + /* Update the counts for each uninterpreted sort. + * For non-existing keys, C++ will create a new element for it, which has + * a default 0 value, before incrementing by 1. */ + usortCardinality[type] = usortCardinality[type] + 1; + } + + collectUSortsToBV(toProcess, usortCardinality, usVarsToBVVars); + + for (size_t i = 0, size = assertions->size(); i < size; ++i) + { + Node old = (*assertions)[i]; + assertions->replace(i, usVarsToBVVars.apply((*assertions)[i])); + Trace("uninterpretedSorts-to-bv") + << " " << old << " => " << (*assertions)[i] << "\n"; + } + } +} + +/* -------------------------------------------------------------------------- */ + Ackermann::Ackermann(PreprocessingPassContext* preprocContext) : PreprocessingPass(preprocContext, "ackermann"), - d_funcToSkolem(preprocContext->getUserContext()) + d_funcToSkolem(preprocContext->getUserContext()), + d_usVarsToBVVars(preprocContext->getUserContext()), + d_logic(preprocContext->getLogicInfo()) { } @@ -215,6 +318,10 @@ PreprocessingPassResult Ackermann::applyInternal( i, d_funcToSkolem.apply((*assertionsToPreprocess)[i])); } + /* replace uninterpreted sorts with bit-vectors */ + usortsToBitVectors( + d_logic, assertionsToPreprocess, d_usortCardinality, d_usVarsToBVVars); + return PreprocessingPassResult::NO_CONFLICT; } diff --git a/src/preprocessing/passes/ackermann.h b/src/preprocessing/passes/ackermann.h index 410dde8b9..4aa26da85 100644 --- a/src/preprocessing/passes/ackermann.h +++ b/src/preprocessing/passes/ackermann.h @@ -38,6 +38,8 @@ namespace passes { using TNodeSet = std::unordered_set; using FunctionToArgsMap = std::unordered_map; +using USortToBVSizeMap = + std::unordered_map; class Ackermann : public PreprocessingPass { @@ -54,6 +56,10 @@ class Ackermann : public PreprocessingPass * - For each f(X) and f(Y) with X = (x1, . . . , xn) and Y = (y1, . . . , yn) * occurring in the input formula, add the following lemma: * (x_1 = y_1 /\ ... /\ x_n = y_n) => f_X = f_Y + * + * - For each uninterpreted sort S, suppose k is the number of variables with + * sort S, then for each such variable X, introduce a fresh variable BV_X + * with BV with size log_2(k)+1 and use it to replace all occurrences of X. */ PreprocessingPassResult applyInternal( AssertionPipeline* assertionsToPreprocess) override; @@ -61,9 +67,15 @@ class Ackermann : public PreprocessingPass private: /* Map each function to a set of terms associated with it */ FunctionToArgsMap d_funcToArgs; - /* Map each function term to the new Skolem variable created by + /* Map each function-application term to the new Skolem variable created by * ackermannization */ theory::SubstitutionMap d_funcToSkolem; + /* Map each variable with uninterpreted sort to the new Skolem BV variable + * created by ackermannization */ + theory::SubstitutionMap d_usVarsToBVVars; + /* Map each uninterpreted sort to the number of variables in this sort. */ + USortToBVSizeMap d_usortCardinality; + LogicInfo d_logic; }; } // namespace passes diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 0276684d6..cb1445b93 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1212,21 +1212,18 @@ void SmtEngine::setDefaults() { } // set options about ackermannization - if (options::produceModels()) + if (options::ackermann() && options::produceModels() + && (d_logic.isTheoryEnabled(THEORY_ARRAYS) + || d_logic.isTheoryEnabled(THEORY_UF))) { - if (options::ackermann() - && (d_logic.isTheoryEnabled(THEORY_ARRAYS) - || d_logic.isTheoryEnabled(THEORY_UF))) + if (options::produceModels.wasSetByUser()) { - if (options::produceModels.wasSetByUser()) - { - throw OptionException(std::string( - "Ackermannization currently does not support model generation.")); - } - Notice() << "SmtEngine: turn off ackermannization to support model" - << "generation" << endl; - options::ackermann.set(false); + throw OptionException(std::string( + "Ackermannization currently does not support model generation.")); } + Notice() << "SmtEngine: turn off ackermannization to support model" + << "generation" << endl; + options::ackermann.set(false); } if (options::ackermann()) @@ -1237,6 +1234,11 @@ void SmtEngine::setDefaults() { "Incremental Ackermannization is currently not supported."); } + if (d_logic.isQuantified()) + { + throw LogicException("Cannot use Ackermannization on quantified formula"); + } + if (d_logic.isTheoryEnabled(THEORY_UF)) { d_logic = d_logic.getUnlockedCopy(); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index c4dfd2593..f4937f8f3 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -170,6 +170,10 @@ set(regress_0_tests regress0/bv/ackermann2.smt2 regress0/bv/ackermann3.smt2 regress0/bv/ackermann4.smt2 + regress0/bv/ackermann5.smt2 + regress0/bv/ackermann6.smt2 + regress0/bv/ackermann7.smt2 + regress0/bv/ackermann8.smt2 regress0/bv/bool-model.smt2 regress0/bv/bool-to-bv-all.smt2 regress0/bv/bool-to-bv-ite.smt2 diff --git a/test/regress/regress0/bv/ackermann5.smt2 b/test/regress/regress0/bv/ackermann5.smt2 new file mode 100644 index 000000000..d29311109 --- /dev/null +++ b/test/regress/regress0/bv/ackermann5.smt2 @@ -0,0 +1,31 @@ +; COMMAND-LINE: --ackermann --no-check-models --no-check-proofs --no-check-unsat-cores +; EXPECT: sat +(set-logic QF_UFBV) + +(declare-sort S 0) +(declare-sort T 0) + +(declare-fun s1 () S) +(declare-fun s2 () S) +(declare-fun t1 () T) +(declare-fun t2 () T) + +(declare-fun a () (_ BitVec 4)) +(declare-fun b () (_ BitVec 4)) + +(declare-fun f (S) (_ BitVec 4)) +(declare-fun g (S) S) +(declare-fun h (T) S) +(declare-fun i (T) T) + +(assert (= (f s1) (bvand a b))) +(assert (= (f s2) (bvand a b))) + +(assert (= (f (g s1)) (f (h (i t1))))) +(assert (= (f (g (h (i t2)))) (f (h (i t2))))) +(assert (= t1 t2)) +(assert (= s1 (h (i t2)))) + +(check-sat) +(exit) + diff --git a/test/regress/regress0/bv/ackermann6.smt2 b/test/regress/regress0/bv/ackermann6.smt2 new file mode 100644 index 000000000..846339f52 --- /dev/null +++ b/test/regress/regress0/bv/ackermann6.smt2 @@ -0,0 +1,31 @@ +; COMMAND-LINE: --ackermann --no-check-models --no-check-proofs --no-check-unsat-cores +; EXPECT: unsat +(set-logic QF_UFBV) + +(declare-sort S 0) +(declare-sort T 0) + +(declare-fun s1 () S) +(declare-fun s2 () S) +(declare-fun t1 () T) +(declare-fun t2 () T) + +(declare-fun a () (_ BitVec 4)) +(declare-fun b () (_ BitVec 4)) + +(declare-fun f (S) (_ BitVec 4)) +(declare-fun g (S) S) +(declare-fun h (T) S) +(declare-fun i (T) T) + +(assert (= (f s1) (bvand a b))) +(assert (= (f s2) (bvand a b))) + +(assert (= (f (g s1)) (f (h (i t1))))) +(assert (not (= (f (g (h (i t2)))) (f (h (i t2)))))) +(assert (= t1 t2)) +(assert (= s1 (h (i t2)))) + +(check-sat) +(exit) + diff --git a/test/regress/regress0/bv/ackermann7.smt2 b/test/regress/regress0/bv/ackermann7.smt2 new file mode 100644 index 000000000..174ad747a --- /dev/null +++ b/test/regress/regress0/bv/ackermann7.smt2 @@ -0,0 +1,26 @@ +; COMMAND-LINE: --ackermann --no-check-models --no-check-proofs --no-check-unsat-cores +; EXPECT: sat +(set-logic QF_UFBV) + +(declare-sort S 0) +(declare-sort T 0) + +(declare-fun s1 () S) +(declare-fun s2 () S) +(declare-fun s3 () S) + +(declare-fun t1 () T) +(declare-fun t2 () T) +(declare-fun t3 () T) + +(assert (not (= s1 s2))) +(assert (not (= s2 s3))) +(assert (not (= s3 s1))) + +(assert (not (= t1 t2))) +(assert (not (= t2 t3))) +(assert (not (= t3 t1))) + +(check-sat) +(exit) + diff --git a/test/regress/regress0/bv/ackermann8.smt2 b/test/regress/regress0/bv/ackermann8.smt2 new file mode 100644 index 000000000..2a424e085 --- /dev/null +++ b/test/regress/regress0/bv/ackermann8.smt2 @@ -0,0 +1,26 @@ +; COMMAND-LINE: --ackermann --no-check-models --no-check-proofs --no-check-unsat-cores +; EXPECT: unsat +(set-logic QF_UFBV) + +(declare-sort S 0) +(declare-sort T 0) + +(declare-fun s1 () S) +(declare-fun s2 () S) +(declare-fun s3 () S) + +(declare-fun a () (_ BitVec 1)) +(declare-fun b () (_ BitVec 1)) +(declare-fun c () (_ BitVec 1)) + +(assert (not (= s1 s2))) +(assert (not (= s2 s3))) +(assert (not (= s3 s1))) + +(assert (not (= a b))) +(assert (not (= b c))) +(assert (not (= c a))) + +(check-sat) +(exit) + diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h index bc5f73435..5af01c0cf 100644 --- a/test/unit/theory/theory_bv_white.h +++ b/test/unit/theory/theory_bv_white.h @@ -68,6 +68,8 @@ public: } void testBitblasterCore() { + d_smt->setLogic("QF_BV"); + d_smt->setOption("bitblast", SExpr("eager")); d_smt->setOption("incremental", SExpr("false")); // Notice that this unit test uses the theory engine of a created SMT