Skip to content

Commit

Permalink
feat: Updating an SMT solver class (#4981)
Browse files Browse the repository at this point in the history 
This pr mostly adds more functionality to `smt_solver::Solver` class,
including

- new options to cvc5 solver config, including verbosity increase and
finite field solver choice
- `default_solver_config` constant so you don't need to initialize it
each time
- `print_assertions` method that converts smt lang to something more
readable and outputs it
- tests for solver class

Also it updates and fixes the symbolic terms classes:

- `^` operation is no longer viable with `FFITerm`, since they are not
compatible
- `!=` operation now uses boolean **NOT** instead of equating the whole
term to `false`
- `std::string` method now uses `smt_solver::stringify_term`
- `!` operator was added to `Bool` class

---------

Co-authored-by: Rumata888 <isennovskiy@gmail.com>
  • Loading branch information
@Sarkoxed @Rumata888
Sarkoxed and Rumata888 authored Mar 8, 2024
1 parent 77954ab commit 4b94d58
Show file tree
Hide file tree
Showing 15 changed files with 351 additions and 72 deletions.
6 changes: 2 additions & 4 deletions barretenberg/cpp/src/barretenberg/smt_verification/smt_bigfield.test.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,8 +41,6 @@ using fq_ct = bn254::BaseField;
using public_witness_ct = bn254::public_witness_ct;
using witness_ct = bn254::witness_ct;

SolverConfiguration config = { true, 0 };

msgpack::sbuffer create_circuit(bool pub_ab, bool ab)
{
StandardCircuitBuilder builder = StandardCircuitBuilder();
Expand Down Expand Up @@ -182,7 +180,7 @@ TEST(bigfield, multiplication_equal)
auto buf = create_circuit(public_a_b, a_neq_b);

CircuitSchema circuit_info = unpack_from_buffer(buf);
Solver s(circuit_info.modulus, config);
Solver s(circuit_info.modulus);
Circuit<FFTerm> circuit(circuit_info, &s);
std::vector<FFTerm> ev = correct_result(circuit, &s);

Expand All @@ -207,7 +205,7 @@ TEST(bigfield, unique_square)

CircuitSchema circuit_info = unpack_from_buffer(buf);

Solver s(circuit_info.modulus, config);
Solver s(circuit_info.modulus);

std::pair<Circuit<FFTerm>, Circuit<FFTerm>> cs =
unique_witness<FFTerm>(circuit_info,
Expand Down
10 changes: 5 additions & 5 deletions barretenberg/cpp/src/barretenberg/smt_verification/smt_examples.test.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@ TEST(circuit_verification, multiplication_true)
auto buf = builder.export_circuit();

smt_circuit::CircuitSchema circuit_info = smt_circuit::unpack_from_buffer(buf);
smt_solver::Solver s(circuit_info.modulus, { true, 0 });
smt_solver::Solver s(circuit_info.modulus);
smt_circuit::Circuit<smt_terms::FFTerm> circuit(circuit_info, &s);
smt_terms::FFTerm a1 = circuit["a"];
smt_terms::FFTerm b1 = circuit["b"];
Expand Down Expand Up @@ -66,7 +66,7 @@ TEST(circuit_verification, multiplication_true_kind)
auto buf = builder.export_circuit();

smt_circuit::CircuitSchema circuit_info = smt_circuit::unpack_from_buffer(buf);
smt_solver::Solver s(circuit_info.modulus, { true, 0 });
smt_solver::Solver s(circuit_info.modulus);
smt_circuit::Circuit<smt_terms::FFTerm> circuit(circuit_info, &s);
smt_terms::FFTerm a1 = circuit["a"];
smt_terms::FFTerm b1 = circuit["b"];
Expand Down Expand Up @@ -97,7 +97,7 @@ TEST(circuit_verification, multiplication_false)
auto buf = builder.export_circuit();

smt_circuit::CircuitSchema circuit_info = smt_circuit::unpack_from_buffer(buf);
smt_solver::Solver s(circuit_info.modulus, { true, 0 });
smt_solver::Solver s(circuit_info.modulus);
smt_circuit::Circuit<smt_terms::FFTerm> circuit(circuit_info, &s);

smt_terms::FFTerm a1 = circuit["a"];
Expand Down Expand Up @@ -140,7 +140,7 @@ TEST(circuit_verifiaction, unique_witness)
auto buf = builder.export_circuit();

smt_circuit::CircuitSchema circuit_info = smt_circuit::unpack_from_buffer(buf);
smt_solver::Solver s(circuit_info.modulus, { true, 0 });
smt_solver::Solver s(circuit_info.modulus);

std::pair<smt_circuit::Circuit<smt_terms::FFTerm>, smt_circuit::Circuit<smt_terms::FFTerm>> cirs =
smt_circuit::unique_witness<smt_terms::FFTerm>(circuit_info, &s, { "ev" }, { "z" });
Expand All @@ -157,7 +157,7 @@ using namespace smt_terms;

TEST(solver_use_case, solver)
{
Solver s("11", { true, 0 }, 10);
Solver s("11", default_solver_config, 10);
FFTerm x = FFTerm::Var("x", &s);
FFTerm y = FFTerm::Var("y", &s);

Expand Down
21 changes: 0 additions & 21 deletions barretenberg/cpp/src/barretenberg/smt_verification/smt_intmod.test.cpp
View file

This file was deleted.

4 changes: 2 additions & 2 deletions barretenberg/cpp/src/barretenberg/smt_verification/smt_polynomials.test.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -120,7 +120,7 @@ TEST(polynomial_evaluation, correct)

CircuitSchema circuit_info = unpack_from_buffer(buf);

Solver s(circuit_info.modulus, { true, 0 });
Solver s(circuit_info.modulus);
Circuit<smt_terms::FFTerm> circuit(circuit_info, &s);
FFTerm ev = polynomial_evaluation(circuit, n, true);

Expand All @@ -143,7 +143,7 @@ TEST(polynomial_evaluation, incorrect)

CircuitSchema circuit_info = unpack_from_buffer(buf);

Solver s(circuit_info.modulus, { true, 0 });
Solver s(circuit_info.modulus);
Circuit<smt_terms::FFTerm> circuit(circuit_info, &s);
FFTerm ev = polynomial_evaluation(circuit, n, false);

Expand Down
170 changes: 168 additions & 2 deletions barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,13 +11,22 @@ namespace smt_solver {
bool Solver::check()
{
cvc5::Result result = this->s.checkSat();
this->res = result.isSat();
this->checked = true;
this->cvc_result = result;

if (result.isUnknown()) {
info("Unknown Result");
}
this->res = result.isSat();
return this->res;
}

/**
* If the system is solvable, extract the values for the given symbolic variables.
* Specify the map to retrieve the values you need using the keys that are convenient for you.
*
* e.g. {"a": a}, where a is a symbolic term with the name "var78".
* The return map will be {"a", value_of_a}
*
* @param terms A map containing pairs (name, symbolic term).
* @return A map containing pairs (name, value).
Expand All @@ -32,9 +41,166 @@ std::unordered_map<std::string, std::string> Solver::model(std::unordered_map<st
}
std::unordered_map<std::string, std::string> resulting_model;
for (auto& term : terms) {
std::string str_val = this->s.getValue(term.second).getFiniteFieldValue();
cvc5::Term val = this->s.getValue(term.second);
std::string str_val;
if (val.isIntegerValue()) {
str_val = val.getIntegerValue();
} else if (val.isFiniteFieldValue()) {
str_val = val.getFiniteFieldValue();
} else {
throw std::invalid_argument("Expected Integer or FiniteField sorts. Got: " + val.getSort().toString());
}
resulting_model.insert({ term.first, str_val });
}
return resulting_model;
}

/**
* If the system is solvable, extract the values for the given symbolic variables.
* The return map will contain the resulting values, which are available by the
* names of the corresponding symbolic variable.
*
* e.g. if the input vector is {a} and a is a term with name var78,
* it will return {"var78": value_of_var78}
*
* @param terms A vector containing symbolic terms.
* @return A map containing pairs (variable name, value).
* */
std::unordered_map<std::string, std::string> Solver::model(std::vector<cvc5::Term>& terms) const
{
if (!this->checked) {
throw std::length_error("Haven't checked yet");
}
if (!this->res) {
throw std::length_error("There's no solution");
}
std::unordered_map<std::string, std::string> resulting_model;
for (auto& term : terms) {
cvc5::Term val = this->s.getValue(term);
std::string str_val;
if (val.isIntegerValue()) {
str_val = val.getIntegerValue();
} else if (val.isFiniteFieldValue()) {
str_val = val.getFiniteFieldValue();
} else {
throw std::invalid_argument("Expected Integer or FiniteField sorts. Got: " + val.getSort().toString());
}
resulting_model.insert({ term.toString(), str_val });
}
return resulting_model;
}

/**
* A simple recursive function that converts native smt language
* to somewhat readable by humans.
*
* e.g. converts
* (or (= a0 #b0000000000) (= a0 #b0000000001)) to ((a0 == 0) || (a0 == 1))
* (= (* (+ a b) c) 10) to ((a + b) * c) == 10
*
* @param term cvc5 term.
* @return Parsed term.
* */
std::string stringify_term(const cvc5::Term& term, bool parenthesis)
{
if (term.getKind() == cvc5::Kind::CONSTANT) {
return term.toString();
}
if (term.getKind() == cvc5::Kind::CONST_FINITE_FIELD) {
return term.getFiniteFieldValue();
}
if (term.getKind() == cvc5::Kind::CONST_INTEGER) {
return term.getIntegerValue();
}
if (term.getKind() == cvc5::Kind::CONST_BOOLEAN) {
std::vector<std::string> bool_res = { "false", "true" };
return bool_res[static_cast<size_t>(term.getBooleanValue())];
}

std::string res;
std::string op;
bool child_parenthesis = true;
switch (term.getKind()) {
case cvc5::Kind::ADD:
case cvc5::Kind::FINITE_FIELD_ADD:
op = " + ";
child_parenthesis = false;
break;
case cvc5::Kind::SUB:
op = " - ";
child_parenthesis = false;
break;
case cvc5::Kind::NEG:
case cvc5::Kind::FINITE_FIELD_NEG:
res = "-";
break;
case cvc5::Kind::MULT:
case cvc5::Kind::FINITE_FIELD_MULT:
op = " * ";
break;
case cvc5::Kind::EQUAL:
op = " == ";
child_parenthesis = false;
break;
case cvc5::Kind::LT:
op = " < ";
break;
case cvc5::Kind::GT:
op = " > ";
break;
case cvc5::Kind::LEQ:
op = " <= ";
break;
case cvc5::Kind::GEQ:
op = " >= ";
break;
case cvc5::Kind::XOR:
op = " ^ ";
break;
case cvc5::Kind::OR:
op = " || ";
break;
case cvc5::Kind::AND:
op = " && ";
break;
case cvc5::Kind::NOT:
res = "!";
break;
case cvc5::Kind::INTS_MODULUS:
op = " % ";
parenthesis = true;
break;
default:
info("Invalid operand :", term.getKind());
break;
}

size_t i = 0;
cvc5::Term child;
for (const auto& t : term) {
if (i == term.getNumChildren() - 1) {
child = t;
break;
}
res += stringify_term(t, child_parenthesis) + op;
i += 1;
}

res = res + stringify_term(child, child_parenthesis);
if (parenthesis) {
return "(" + res + ")";
}
return res;
}

/**
* Output assertions in human readable format.
*
* */
void Solver::print_assertions() const
{
for (auto& t : this->s.getAssertions()) {
info(stringify_term(t));
}
}
}; // namespace smt_solver
Loading

0 comments on commit 4b94d58

Please sign in to comment.