From 0efb169b74c699c5978aa92006b9cb1387bfc901 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 4 Aug 2018 15:18:13 +0100 Subject: [PATCH 1/2] remove AIGs --- src/cbmc/cbmc_solvers.cpp | 1 - src/cbmc/cbmc_solvers.h | 1 - src/solvers/Makefile | 2 - src/solvers/prop/aig.cpp | 183 ----------- src/solvers/prop/aig.h | 157 --------- src/solvers/prop/aig_prop.cpp | 598 ---------------------------------- src/solvers/prop/aig_prop.h | 133 -------- 7 files changed, 1075 deletions(-) delete mode 100644 src/solvers/prop/aig.cpp delete mode 100644 src/solvers/prop/aig.h delete mode 100644 src/solvers/prop/aig_prop.cpp delete mode 100644 src/solvers/prop/aig_prop.h diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp index 31e5793ce3..b71b6c320f 100644 --- a/src/cbmc/cbmc_solvers.cpp +++ b/src/cbmc/cbmc_solvers.cpp @@ -23,7 +23,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include "bv_cbmc.h" diff --git a/src/cbmc/cbmc_solvers.h b/src/cbmc/cbmc_solvers.h index 66df55eca8..2a852221fc 100644 --- a/src/cbmc/cbmc_solvers.h +++ b/src/cbmc/cbmc_solvers.h @@ -23,7 +23,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include diff --git a/src/solvers/Makefile b/src/solvers/Makefile index aeabd7e28e..a199c95403 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -146,8 +146,6 @@ SRC = $(BOOLEFORCE_SRC) \ floatbv/float_approximation.cpp \ lowering/popcount.cpp \ miniBDD/miniBDD.cpp \ - prop/aig.cpp \ - prop/aig_prop.cpp \ prop/bdd_expr.cpp \ prop/cover_goals.cpp \ prop/literal.cpp \ diff --git a/src/solvers/prop/aig.cpp b/src/solvers/prop/aig.cpp deleted file mode 100644 index a164b379db..0000000000 --- a/src/solvers/prop/aig.cpp +++ /dev/null @@ -1,183 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -#include "aig.h" - -#include -#include -#include - -std::string aigt::label(nodest::size_type v) const -{ - return "var("+std::to_string(v)+")"; -} - -std::string aigt::dot_label(nodest::size_type v) const -{ - return "var("+std::to_string(v)+")"; -} - -void aigt::get_terminals(terminalst &terminals) const -{ - for(nodest::size_type n=0; nsecond; // already done - - assert(n &ta= - get_terminals_rec(node.a.var_no(), terminals); - t.insert(ta.begin(), ta.end()); - } - - if(!node.b.is_constant()) - { - const std::set &tb= - get_terminals_rec(node.b.var_no(), terminals); - t.insert(tb.begin(), tb.end()); - } - } - else // this is a terminal - { - t.insert(n); - } - - return t; -} - -void aigt::print( - std::ostream &out, - literalt a) const -{ - if(a==const_literal(false)) - { - out << "FALSE"; - return; - } - else if(a==const_literal(true)) - { - out << "TRUE"; - return; - } - - literalt::var_not node_nr=a.var_no(); - - { - const aig_nodet &node=nodes[node_nr]; - - if(node.is_and()) - { - if(a.sign()) - out << "!("; - print(out, node.a); - out << " & "; - print(out, node.b); - if(a.sign()) - out << ")"; - } - else if(node.is_var()) - { - if(a.sign()) - out << "!"; - out << label(node_nr);\ - } - else - { - if(a.sign()) - out << "!"; - out << "unknown(" << node_nr << ")"; - } - } -} - -void aigt::output_dot_node( - std::ostream &out, - nodest::size_type v) const -{ - const aig_nodet &node=nodes[v]; - - if(node.is_and()) - { - out << v << " [label=\"" << v << "\"]" << "\n"; - output_dot_edge(out, v, node.a); - output_dot_edge(out, v, node.b); - } - else // the node is a terminal - { - out << v << " [label=\"" << dot_label(v) << "\"" - << ",shape=box]" << "\n"; - } -} - -void aigt::output_dot_edge( - std::ostream &out, - nodest::size_type v, - literalt l) const -{ - if(l.is_true()) - { - out << "TRUE -> " << v; - } - else if(l.is_false()) - { - out << "TRUE -> " << v; - out << " [arrowhead=odiamond]"; - } - else - { - out << l.var_no() << " -> " << v; - if(l.sign()) - out << " [arrowhead=odiamond]"; - } - - out << "\n"; -} - -void aigt::output_dot(std::ostream &out) const -{ - // constant TRUE - out << "TRUE [label=\"TRUE\", shape=box]" << "\n"; - - // now the nodes - for(nodest::size_type n=0; n -#include -#include - -#include - -class aig_nodet -{ -public: - literalt a, b; - - aig_nodet() - { - } - - bool is_and() const - { - return a.var_no()!=literalt::unused_var_no(); - } - - bool is_var() const - { - return a.var_no()==literalt::unused_var_no(); - } - - void make_and(literalt _a, literalt _b) - { - a=_a; - b=_b; - } - - void make_var() - { - a.set(literalt::unused_var_no(), false); - } -}; - -class aigt -{ -public: - aigt() - { - } - - ~aigt() - { - } - - typedef aig_nodet nodet; - typedef std::vector nodest; - nodest nodes; - - void clear() - { - nodes.clear(); - } - - typedef std::set terminal_sett; - typedef std::map terminalst; - - // produces the support set - // should get re-written - void get_terminals(terminalst &terminals) const; - - const aig_nodet &get_node(literalt l) const - { - return nodes[l.var_no()]; - } - - aig_nodet &get_node(literalt l) - { - return nodes[l.var_no()]; - } - - nodest::size_type number_of_nodes() const - { - return nodes.size(); - } - - void swap(aigt &g) - { - nodes.swap(g.nodes); - } - - literalt new_node() - { - nodes.push_back(aig_nodet()); - literalt l; - l.set(nodes.size()-1, false); - return l; - } - - literalt new_var_node() - { - literalt l=new_node(); - nodes.back().make_var(); - return l; - } - - literalt new_and_node(literalt a, literalt b) - { - literalt l=new_node(); - nodes.back().make_and(a, b); - return l; - } - - bool empty() const - { - return nodes.empty(); - } - - void print(std::ostream &out) const; - void print(std::ostream &out, literalt a) const; - void output_dot_node(std::ostream &out, nodest::size_type v) const; - void output_dot_edge( - std::ostream &out, nodest::size_type v, literalt l) const; - void output_dot(std::ostream &out) const; - - std::string label(nodest::size_type v) const; - std::string dot_label(nodest::size_type v) const; - -protected: - const std::set &get_terminals_rec( - literalt::var_not n, - terminalst &terminals) const; -}; - -std::ostream &operator << (std::ostream &, const aigt &); - -class aig_plus_constraintst:public aigt -{ -public: - typedef std::vector constraintst; - constraintst constraints; - - void clear() - { - aigt::clear(); - constraints.clear(); - } -}; - -#endif // CPROVER_SOLVERS_PROP_AIG_H diff --git a/src/solvers/prop/aig_prop.cpp b/src/solvers/prop/aig_prop.cpp deleted file mode 100644 index 9b8e90427e..0000000000 --- a/src/solvers/prop/aig_prop.cpp +++ /dev/null @@ -1,598 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -#include "aig_prop.h" - -#include -#include - -// Tries to compact AIGs corresponding to xor and equality -// Needed to match the performance of the native CNF back-end. -#define USE_AIG_COMPACT - -// Use the Plaisted-Greenbaum encoding, again, needed to match the -// native CNF back-end. -#define USE_PG - -literalt aig_prop_baset::land(const bvt &bv) -{ - literalt literal=const_literal(true); - - // Introduces N-1 extra nodes for N bits - // See convert_node for where this overhead is removed - forall_literals(it, bv) - literal=land(*it, literal); - - return literal; -} - -literalt aig_prop_baset::lor(const bvt &bv) -{ - literalt literal=const_literal(true); - - // Introduces N-1 extra nodes for N bits - // See convert_node for where this overhead is removed - forall_literals(it, bv) - literal=land(neg(*it), literal); - - return neg(literal); -} - -literalt aig_prop_baset::lxor(const bvt &bv) -{ - literalt literal=const_literal(false); - - forall_literals(it, bv) - literal=lxor(*it, literal); - - return literal; -} - -literalt aig_prop_baset::land(literalt a, literalt b) -{ - if(a.is_true() || b.is_false()) - return b; - if(b.is_true() || a.is_false()) - return a; - - if(a==neg(b)) - return const_literal(false); - if(a==b) - return a; - - return dest.new_and_node(a, b); -} - -literalt aig_prop_baset::lor(literalt a, literalt b) -{ - return neg(land(neg(a), neg(b))); // De Morgan's -} - -literalt aig_prop_baset::lxor(literalt a, literalt b) -{ - if(a.is_false()) - return b; - if(b.is_false()) - return a; - if(a.is_true()) - return neg(b); - if(b.is_true()) - return neg(a); - - if(a==b) - return const_literal(false); - if(a==neg(b)) - return const_literal(true); - - // This produces up to three nodes! - // See convert_node for where this overhead is removed - return lor(land(a, neg(b)), land(neg(a), b)); -} - -literalt aig_prop_baset::lnand(literalt a, literalt b) -{ - return !land(a, b); -} - -literalt aig_prop_baset::lnor(literalt a, literalt b) -{ - return !lor(a, b); -} - -literalt aig_prop_baset::lequal(literalt a, literalt b) -{ - return !lxor(a, b); -} - -literalt aig_prop_baset::limplies(literalt a, literalt b) -{ - return lor(neg(a), b); -} - -literalt aig_prop_baset::lselect(literalt a, literalt b, literalt c) -{ // a?b:c=(a AND b) OR (/a AND c) - if(a.is_true()) - return b; - if(a.is_false()) - return c; - if(b==c) - return b; - - // This produces unnecessary clauses and variables - // See convert_node for where this overhead is removed - - return lor(land(a, b), land(neg(a), c)); -} - -void aig_prop_baset::set_equal(literalt a, literalt b) -{ -#ifdef USE_AIG_COMPACT - // The compact encoding should reduce this - l_set_to_true(lequal(a, b)); - -#else - // we produce two constraints: - // a|!b !a|b - - l_set_to_true(lor(pos(a), neg(b))); - l_set_to_true(lor(neg(a), pos(b))); -#endif -} - -tvt aig_prop_solvert::l_get(literalt a) const -{ - return solver.l_get(a); -} - -propt::resultt aig_prop_solvert::prop_solve() -{ - status() << "converting AIG, " - << aig.nodes.size() << " nodes" << eom; - convert_aig(); - - return solver.prop_solve(); -} - -/// Compute the phase information needed for Plaisted-Greenbaum encoding -/// \par parameters: Two vectors of bools of size aig.nodes.size() -/// \return These vectors filled in with per node phase information -void aig_prop_solvert::compute_phase( - std::vector &n_pos, - std::vector &n_neg) -{ - std::stack queue; - - // Get phases of constraints - for(aig_plus_constraintst::constraintst::const_iterator - c_it=aig.constraints.begin(); - c_it!=aig.constraints.end(); - c_it++) - queue.push(*c_it); - - while(!queue.empty()) - { - literalt l=queue.top(); - queue.pop(); - - if(l.is_constant()) - continue; - - bool sign=l.sign(); - unsigned var_no=l.var_no(); - - // already set? - if(sign?n_neg[var_no]:n_pos[var_no]) - continue; // done already - - // set - sign?n_neg[var_no]=1:n_pos[var_no]=1; - - const aigt::nodet &node=aig.nodes[var_no]; - - if(node.is_and()) - { - queue.push(node.a^sign); - queue.push(node.b^sign); - } - } - - // Count - unsigned pos_only=0, neg_only=0, mixed=0; - - for(unsigned n=0; n &p_usage_count, - std::vector &n_usage_count) -{ - for(aig_plus_constraintst::constraintst::const_iterator - c_it=aig.constraints.begin(); - c_it!=aig.constraints.end(); - c_it++) - { - if(!((*c_it).is_constant())) - { - if((*c_it).sign()) - { - ++n_usage_count[(*c_it).var_no()]; - } - else - { - ++p_usage_count[(*c_it).var_no()]; - } - } - } - - for(unsigned n=0; n=2) - { - ++usedTwicePositive; - } - else if(n_usage_count[n]>=2) - { - ++usedTwiceNegative; - } - else - { - assert(p_usage_count[n]==1 && n_usage_count[n]==1); - ++usedTwiceMixed; - } - break; - case 3: ++usedThreeTimes; break; - default: ++usedMore; break; - } - } - - statistics() << "Unused: " << unused << " " - << "Used once: " << usedOncePositive + usedOnceNegative - << " (P: " << usedOncePositive - << ", N: " << usedOnceNegative << ") " - << "Used twice: " - << usedTwicePositive + usedTwiceNegative + usedTwiceMixed - << " (P: " << usedTwicePositive - << ", N: " << usedTwiceNegative - << ", M: " << usedTwiceMixed << ") " - << "Used three times: " << usedThreeTimes << " " - << "Used more: " << usedMore - << eom; - #endif -} - -/// Convert one AIG node, including special handling of a couple of cases -/// \par parameters: The node to convert, the phases required and the usage -/// counts. -/// \return The node converted to CNF in the solver object. -void aig_prop_solvert::convert_node( - unsigned n, - const aigt::nodet &node, - bool n_pos, bool n_neg, - std::vector &p_usage_count, - std::vector &n_usage_count) -{ - if(p_usage_count[n]>0 || n_usage_count[n]>0) - { - literalt o=literalt(n, false); - bvt body(2); - body[0]=node.a; - body[1]=node.b; - -#ifdef USE_AIG_COMPACT - // Inline positive literals - // This should remove the overhead introduced by land and lor for bvt - - for(bvt::size_type i=0; i < body.size(); i++) - { - literalt l=body[i]; - - if(!l.sign() && // Used positively... - aig.nodes[l.var_no()].is_and() && // ... is a gate ... - p_usage_count[l.var_no()] == 1 && // ... only used here. - n_usage_count[l.var_no()] == 0) - { - const aigt::nodet &rep=aig.nodes[l.var_no()]; - body[i]=rep.a; - body.push_back(rep.b); - --i; // Repeat the process - --p_usage_count[l.var_no()]; // Supress generation of inlined node - } - } - - // TODO : Could check the array for duplicates / complementary literals - // but this should be found by the SAT preprocessor. - // TODO : Likewise could find things that are constrained, esp the output - // and backwards constant propagate. Again may not be worth it. - - // lxor and lselect et al. are difficult to express in AIGs. - // Doing so introduces quite a bit of overhead. - // This should recognise the AIGs they produce and - // handle them in a more efficient way. - - // Recognise something of the form: - // - // neg(o)=lor(land(a,b), land(neg(a),c)) - // o =land(lneg(land(a,b)), lneg(land(neg(a),c))) - // - // Note that lxor and lselect generate the negation of this - // but will still be recognised because the negation is - // recorded where it is used - - if(body.size() == 2 && body[0].sign() && body[1].sign()) - { - const aigt::nodet &left=aig.nodes[body[0].var_no()]; - const aigt::nodet &right=aig.nodes[body[1].var_no()]; - - if(left.is_and() && right.is_and()) - { - if(left.a==neg(right.a)) - { - if(p_usage_count[body[0].var_no()]==0 && - n_usage_count[body[0].var_no()]==1 && - p_usage_count[body[1].var_no()]==0 && - n_usage_count[body[1].var_no()]==1) - { - bvt lits(3); - - if(n_neg) - { - lits[0]=left.a; - lits[1]=right.b; - lits[2]=o; - solver.lcnf(lits); - - lits[0]=neg(left.a); - lits[1]=left.b; - lits[2]=o; - solver.lcnf(lits); - } - - if(n_pos) - { - lits[0]=left.a; - lits[1]=neg(right.b); - lits[2]=neg(o); - solver.lcnf(lits); - - lits[0]=neg(left.a); - lits[1]=neg(left.b); - lits[2]=neg(o); - solver.lcnf(lits); - } - - // Supress generation - --n_usage_count[body[0].var_no()]; - --n_usage_count[body[1].var_no()]; - - return; - } - } - } - } - - - // Likewise, carry has an improved encoding which is generated - // by the CNF encoding - if(body.size() == 3 && body[0].sign() && body[1].sign() && body[2].sign()) - { - const aigt::nodet &left=aig.nodes[body[0].var_no()]; - const aigt::nodet &mid=aig.nodes[body[1].var_no()]; - const aigt::nodet &right=aig.nodes[body[2].var_no()]; - - if(left.is_and() && mid.is_and() && right.is_and()) - { - if(p_usage_count[body[0].var_no()]==0 && - n_usage_count[body[0].var_no()]==1 && - p_usage_count[body[1].var_no()]==0 && - n_usage_count[body[1].var_no()]==1 && - p_usage_count[body[2].var_no()]==0 && - n_usage_count[body[2].var_no()]==1) - { - literalt a=left.a; - literalt b=left.b; - literalt c=mid.a; - - if(a==right.b && b==mid.b && c==right.a) - { - // A (negative) carry -- 1 if at most one input is 1 - bvt lits(3); - - if(n_neg) - { - lits[0]=a; - lits[1]=b; - lits[2]=o; - solver.lcnf(lits); - - lits[0]=a; - lits[1]=c; - lits[2]=o; - solver.lcnf(lits); - - lits[0]=b; - lits[1]=c; - lits[2]=o; - solver.lcnf(lits); - } - - if(n_pos) - { - lits[0]=neg(a); - lits[1]=neg(b); - lits[2]=neg(o); - solver.lcnf(lits); - - lits[0]=neg(a); - lits[1]=neg(c); - lits[2]=neg(o); - solver.lcnf(lits); - - lits[0]=neg(b); - lits[1]=neg(c); - lits[2]=neg(o); - solver.lcnf(lits); - } - - // Supress generation - --n_usage_count[body[0].var_no()]; - --n_usage_count[body[1].var_no()]; - --n_usage_count[body[2].var_no()]; - - return; - } - } - } - } - - // TODO : these special cases are fragile and could be improved. - // They don't handle cases where the construction is partially constant - // folded. Also the usage constraints are sufficient for improvement - // but reductions may still be possible with looser restrictions. -#endif - - if(n_pos) - { - bvt lits(2); - lits[1]=neg(o); - - forall_literals(it, body) - { - lits[0]=pos(*it); - solver.lcnf(lits); - } - } - - if(n_neg) - { - bvt lits; - - forall_literals(it, body) - lits.push_back(neg(*it)); - - lits.push_back(pos(o)); - solver.lcnf(lits); - } - } -} - -void aig_prop_solvert::convert_aig() -{ - // 1. Do variables - while(solver.no_variables()<=aig.nodes.size()) - solver.new_variable(); - - // Usage count for inlining - - std::vector p_usage_count; - std::vector n_usage_count; - p_usage_count.resize(aig.nodes.size(), 0); - n_usage_count.resize(aig.nodes.size(), 0); - - this->usage_count(p_usage_count, n_usage_count); - - - #ifdef USE_PG - // Get phases - std::vector n_pos, n_neg; - n_pos.resize(aig.nodes.size(), false); - n_neg.resize(aig.nodes.size(), false); - - this->compute_phase(n_pos, n_neg); - #endif - - // 2. Do nodes - for(std::size_t n=aig.nodes.size() - 1; n!=0; n--) - { - if(aig.nodes[n].is_and()) - { -#ifdef USE_PG - convert_node( - n, aig.nodes[n], n_pos[n], n_neg[n], p_usage_count, n_usage_count); -#else - convert_node(n, aig.nodes[n], true, true, p_usage_count, n_usage_count); -#endif - } - } - // Skip zero as it is not used or a valid literal - - - // 3. Do constraints - for(const auto &c_it : aig.constraints) - solver.l_set_to(c_it, true); - - // HACK! - aig.nodes.clear(); -} diff --git a/src/solvers/prop/aig_prop.h b/src/solvers/prop/aig_prop.h deleted file mode 100644 index 335f224747..0000000000 --- a/src/solvers/prop/aig_prop.h +++ /dev/null @@ -1,133 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - - -#ifndef CPROVER_SOLVERS_PROP_AIG_PROP_H -#define CPROVER_SOLVERS_PROP_AIG_PROP_H - -#include - -#include -#include - -#include "aig.h" - -class aig_prop_baset:public propt -{ -public: - explicit aig_prop_baset(aigt &_dest):dest(_dest) - { - } - - bool has_set_to() const override { return false; } - bool cnf_handled_well() const override { return false; } - - literalt land(literalt a, literalt b) override; - literalt lor(literalt a, literalt b) override; - literalt land(const bvt &bv) override; - literalt lor(const bvt &bv) override; - void lcnf(const bvt &clause) override { assert(false); } - literalt lxor(literalt a, literalt b) override; - literalt lxor(const bvt &bv) override; - literalt lnand(literalt a, literalt b) override; - literalt lnor(literalt a, literalt b) override; - literalt lequal(literalt a, literalt b) override; - literalt limplies(literalt a, literalt b) override; - literalt lselect(literalt a, literalt b, literalt c) override; // a?b:c - void set_equal(literalt a, literalt b) override; - - void l_set_to(literalt a, bool value) override { assert(false); } - - literalt new_variable() override - { - return dest.new_node(); - } - - size_t no_variables() const override - { return dest.number_of_nodes(); } - - const std::string solver_text() override - { return "conversion into and-inverter graph"; } - - tvt l_get(literalt a) const override - { assert(0); return tvt::unknown(); } - - resultt prop_solve() override - { assert(0); return resultt::P_ERROR; } - -protected: - aigt &dest; -}; - -class aig_prop_constraintt:public aig_prop_baset -{ -public: - explicit aig_prop_constraintt(aig_plus_constraintst &_dest): - aig_prop_baset(_dest), - dest(_dest) - { - } - - aig_plus_constraintst &dest; - bool has_set_to() const override { return true; } - - void lcnf(const bvt &clause) override - { - l_set_to_true(lor(clause)); - } - - void l_set_to(literalt a, bool value) override - { - dest.constraints.push_back(a^!value); - } -}; - -class aig_prop_solvert:public aig_prop_constraintt -{ -public: - explicit aig_prop_solvert(propt &_solver): - aig_prop_constraintt(aig), - solver(_solver) - { - } - - aig_plus_constraintst aig; - - const std::string solver_text() override - { - return - "conversion into and-inverter graph followed by "+ - solver.solver_text(); - } - - tvt l_get(literalt a) const override; - resultt prop_solve() override; - - void set_message_handler(message_handlert &m) override - { - aig_prop_constraintt::set_message_handler(m); - solver.set_message_handler(m); - } - -protected: - propt &solver; - - void convert_aig(); - void usage_count( - std::vector &p_usage_count, std::vector &n_usage_count); - void compute_phase(std::vector &n_pos, std::vector &n_neg); - void convert_node( - unsigned n, - const aigt::nodet &node, - bool n_pos, - bool n_neg, - std::vector &p_usage_count, - std::vector &n_usage_count); -}; - -#endif // CPROVER_SOLVERS_PROP_AIG_PROP_H From d42020ba42a6f8c4e72869cf0c727ddfb325841b Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 6 Aug 2018 13:37:31 +0100 Subject: [PATCH 2/2] remove --aig option --- src/cbmc/cbmc_parse_options.cpp | 3 --- src/cbmc/cbmc_parse_options.h | 2 +- 2 files changed, 1 insertion(+), 4 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index f5074b6b54..8f6e92cb26 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -309,9 +309,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) "max-node-refinement", cmdline.get_value("max-node-refinement")); - if(cmdline.isset("aig")) - options.set_option("aig", true); - // SMT Options if(cmdline.isset("smt1")) diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 5c9cd1c463..d36f976573 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -52,7 +52,7 @@ class optionst; "(string-printable)" \ "(string-max-length):" \ "(string-max-input-length):" \ - "(aig)(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \ + "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \ "(little-endian)(big-endian)" \ OPT_SHOW_GOTO_FUNCTIONS \ OPT_SHOW_PROPERTIES \