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.
**/
#include "preprocessing/passes/ackermann.h"
-
+#include <cmath>
#include "base/check.h"
+#include "expr/node_algorithm.h"
#include "options/options.h"
using namespace CVC4;
/* -------------------------------------------------------------------------- */
+/* 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<size_t>(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<TNode, TNodeHashFunction>& 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<TNode, TNodeHashFunction> getVarsWithUSorts(
+ AssertionPipeline* assertions)
+{
+ std::unordered_set<TNode, TNodeHashFunction> res;
+
+ for (const Node& assertion : assertions->ref())
+ {
+ std::unordered_set<TNode, TNodeHashFunction> 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<TNode, TNodeHashFunction> 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())
{
}
i, d_funcToSkolem.apply((*assertionsToPreprocess)[i]));
}
+ /* replace uninterpreted sorts with bit-vectors */
+ usortsToBitVectors(
+ d_logic, assertionsToPreprocess, d_usortCardinality, d_usVarsToBVVars);
+
return PreprocessingPassResult::NO_CONFLICT;
}
using TNodeSet = std::unordered_set<TNode, TNodeHashFunction>;
using FunctionToArgsMap =
std::unordered_map<TNode, TNodeSet, TNodeHashFunction>;
+using USortToBVSizeMap =
+ std::unordered_map<TypeNode, size_t, TypeNode::HashFunction>;
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;
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
}
// 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())
"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();
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
--- /dev/null
+; 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)
+
--- /dev/null
+; 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)
+
--- /dev/null
+; 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)
+
--- /dev/null
+; 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)
+
}
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
projects / cvc5.git / commitdiff