-
Notifications
You must be signed in to change notification settings - Fork 43
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
* Working on flex/bison files * First pass on driver * First pass on smtlibparser.yy * remove unnecessary file * First pass on smtlibscanner from calc++ example * Update Makefile * Minor * Add test * Various fixes * Fix YY_NULL issue * Pass text through for symbol * Create specific case for set-logic * Fix top-level of grammar and add assert * Remove old files * Rename: smtlibscanner.ll -> smtlibscanner.l because uses C * Add Bool, Int, and Real sorts, and declare-const * use getters and try text in sorts * Add a solver to the driver * Basic sorts working * declare-const working * Put SmtLibDriver in smt namespace * Add lookup_primop feature * Some clean up and add indprefix * Some progress on creating terms * Support assert and check-sat * Clean up and add some arithmetic operators * Add boolean operators * Add declare-fun * Add push/pop * Add true/false * Add set-option and fix for true/false * Add check-sat-assuming and fix spacing * WIP for define-fun -- includes mid-rule actions to set current command * First pass on define-fun (UNTESTED) * More WIP on define-fun * Remove some debug prints * Some fixes for define-fun * Fix location tracking * Ignore comments * Remove some debug prints * Add virtual wrapper functions for commands in SmtLibDriver * Minor * Fix for declare-fun with no arguments * Add exit command * Rename: OPT -> KEYWORD * Support quote and pipe for strings/symbols * Fix in pipe-quoted string * use less character sets in lexer * Use virtual functions for set-* commands * Allow number or string in set-info * Some simplifications * Rename file: test-parser -> smt-switch-parser-cvc4 * Minor changes to main * Compile static non-debug * Turn off flex debugging * Add bitvector sort * Rename: INTEGER -> NAT * WIP BV Operators * Fix for bvop scanner and better error for unknown function * Add support for binary / hex strings * Add support for (_ bv... format * Minor * Add array sort * Add select/store * Add support for as const * Add support for indexed operators * Rename: SmtLibDriver -> SmtLibReader * Put SmtLibReader in CMake -- not yet guarded by an option! * Make SmtLibReader optional * Include bison-generated header in install * Update Makefile * Remove the temporary test files * Use context-dependent map for args * Rename: context -> scope * Use scoped map for arg mapping * WIP for quantifier support * Only use lookup_symbol * Remove unused str_to_command * Fix quantifier scope (pop) and remove unnecessary current_command infrastructure * License headers * Don't install SmtLibReader headers if built without it * Allow optional sort for define-fun * Define-fun with no args is just an alias symbol * Fix for bvashr * Allow more characters in symbols * Require sort for define-fun * Rename: symbols_ -> global_symbols_ * Add support for let bindings * Fix: pop scope after let binding * Support scoping for symbolic constants * Handle Minus/Negate difference * Fix: explicitly use reference when adding to set * Escape quote * Increment location according to newlines in string literals * Update comment * Remove addressed issue * Return definition without substituting if there are no arguments * apply_define_fun requires arguments * Fix hex regex * format * Add newline at end of file * Remove old TODO comments
- Loading branch information
Showing
7 changed files
with
1,278 additions
and
4 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,263 @@ | ||
| /********************* */ | ||
| /*! \file smtlib_reader.h | ||
| ** \verbatim | ||
| ** Top contributors (to current version): | ||
| ** Makai Mann | ||
| ** This file is part of the smt-switch project. | ||
| ** Copyright (c) 2020 by the authors listed in the file AUTHORS | ||
| ** in the top-level source directory) and their institutional affiliations. | ||
| ** All rights reserved. See the file LICENSE in the top-level source | ||
| ** directory for licensing information.\endverbatim | ||
| ** | ||
| ** \brief Driver for reading SMT-LIB files. Depends on flex/bison | ||
| ** | ||
| ** | ||
| **/ | ||
|
|
||
| #pragma once | ||
|
|
||
| #include <string> | ||
| #include <unordered_map> | ||
|
|
||
| #include "smt.h" | ||
| #include "smtlibparser.h" | ||
|
|
||
| #define YY_DECL yy::parser::symbol_type yylex(smt::SmtLibReader & drv) | ||
| YY_DECL; | ||
|
|
||
| namespace smt { | ||
|
|
||
| /** Used to keep track of which command is currently being parsed */ | ||
| enum Command | ||
| { | ||
| SETLOGIC = 0, | ||
| SETOPT, | ||
| SETINFO, | ||
| DECLARECONST, | ||
| DECLAREFUN, | ||
| DEFINEFUN, | ||
| ASSERT, | ||
| CHECKSAT, | ||
| CHECKSATASSUMING, | ||
| PUSH, | ||
| POP, | ||
| NONE /** this must stay at the end -- | ||
| can also be used for the number of Command enums */ | ||
| }; | ||
|
|
||
| /** Basic scoped symbol map | ||
| * Used for arguments and parameters that have limited scope | ||
| * Does not support shadowing within the same mapping scope | ||
| * e.g. forall x . P(x) -> exists x. Q(x) | ||
| * is not supported | ||
| */ | ||
| class UnorderedScopedSymbolMap | ||
| { | ||
| public: | ||
| UnorderedScopedSymbolMap() | ||
| { | ||
| // allow some symbols at 0 | ||
| symbols_.push_back({}); | ||
| } | ||
|
|
||
| size_t current_scope() { return symbols_.size() - 1; } | ||
|
|
||
| void add_mapping(const std::string & sym, const smt::Term & t) | ||
| { | ||
| if (symbol_map_.find(sym) != symbol_map_.end()) | ||
| { | ||
| throw SmtException("Repeated symbol: " + sym); | ||
| } | ||
| symbol_map_[sym] = t; | ||
| symbols_.back().insert(sym); | ||
| } | ||
|
|
||
| void push_scope() { symbols_.push_back({}); } | ||
|
|
||
| void pop_scope() | ||
| { | ||
| assert(current_scope()); | ||
| for (const auto & sym : symbols_.back()) | ||
| { | ||
| symbol_map_.erase(sym); | ||
| } | ||
| symbols_.pop_back(); | ||
| } | ||
|
|
||
| smt::Term get_symbol(const std::string & sym) { return symbol_map_.at(sym); } | ||
|
|
||
| private: | ||
| std::vector<std::unordered_set<std::string>> symbols_; | ||
| std::unordered_map<std::string, smt::Term> symbol_map_; | ||
| }; | ||
|
|
||
| class SmtLibReader | ||
| { | ||
| public: | ||
| SmtLibReader(smt::SmtSolver & solver); | ||
|
|
||
| int parse(const std::string & f); | ||
| // The name of the file being parsed. | ||
| std::string file; | ||
|
|
||
| void scan_begin(); | ||
| void scan_end(); | ||
|
|
||
| /* Override-able functions corresponding to SMT-LIB commands */ | ||
|
|
||
| virtual void set_logic(const std::string & logic); | ||
|
|
||
| virtual void set_opt(const std::string & key, const std::string & val); | ||
|
|
||
| virtual void set_info(const std::string & key, const std::string & val); | ||
|
|
||
| virtual void assert_formula(const smt::Term & assertion); | ||
|
|
||
| virtual Result check_sat(); | ||
|
|
||
| virtual Result check_sat_assuming(const smt::TermVec & assumptions); | ||
|
|
||
| /** Pushes num contexts in the solver and the global symbol map | ||
| * If overriding, make sure to push scopes in global_symbols_ | ||
| * or consider calling this version of the function also | ||
| */ | ||
| virtual void push(uint64_t num = 1); | ||
|
|
||
| /** Pops num contexts in the solver and the global symbol map | ||
| * If overriding, make sure to pop scopes in global_symbols_ | ||
| * or consider calling this version of the function also | ||
| */ | ||
| virtual void pop(uint64_t num = 1); | ||
|
|
||
| /* getters and setters */ | ||
| yy::location & location() { return location_; } | ||
|
|
||
| smt::SmtSolver & solver() { return solver_; } | ||
|
|
||
| /** Pushes a scope for a new quantifier binding or define-fun arguments | ||
| */ | ||
| void push_scope(); | ||
|
|
||
| /** Pushes a scope from quantifier binding or define-fun arguments | ||
| */ | ||
| void pop_scope(); | ||
|
|
||
| size_t current_scope() { return arg_param_map_.current_scope(); } | ||
|
|
||
| /* Methods for use in flex/bison generated code */ | ||
|
|
||
| /** Look up a symbol by name | ||
| * Returns a null term if there is no known symbol | ||
| * with that name | ||
| * @return term | ||
| */ | ||
| smt::Term lookup_symbol(const std::string & sym); | ||
|
|
||
| /** Creates a new symbol | ||
| * This is a light wrapper around solver_->make_symbol | ||
| * s.t. you can look up the symbol by name later | ||
| * see lookup_symbol | ||
| * @param name the name of the symbol | ||
| * @param sort the sort of the symbol | ||
| */ | ||
| void new_symbol(const std::string & name, const smt::Sort & sort); | ||
|
|
||
| /** Look up a primitive operator by a string | ||
| * @param str the string representation of this PrimOp | ||
| * @return the associated PrimOp | ||
| * throws an exception if there's no match | ||
| */ | ||
| PrimOp lookup_primop(const std::string & str); | ||
|
|
||
| /** Create a define-fun macro | ||
| * @param name the name of the define-fun | ||
| * @param the definition | ||
| * @param the arguments to the define-fun | ||
| * stored in defs_ and def_args_ | ||
| */ | ||
| void define_fun(const std::string & name, | ||
| const smt::Term & def, | ||
| const smt::TermVec & args = {}); | ||
|
|
||
| /** Apply a define fun | ||
| * @param defname the name of the define-fun | ||
| * @param args the arguments to apply it to | ||
| * the parameter args from the define-fun | ||
| * declaration will be replaced by these arguments | ||
| */ | ||
| Term apply_define_fun(const std::string & defname, const smt::TermVec & args); | ||
|
|
||
| /** Helper function for define-fun - similar to new_symbol | ||
| * Associates an argument with a temporary symbol for | ||
| * define-fun arguments | ||
| * Renames the arguments to avoid polluting global symbols | ||
| * Stores these in a separate data structure from symbols | ||
| * @param name the name of the argument | ||
| * @param sort the sort of the argument | ||
| * @return the renamed term | ||
| * Note: creates new renamed variables as needed | ||
| * These aren't used except in the definition and will always | ||
| * be substituted for | ||
| */ | ||
| Term register_arg(const std::string & name, const smt::Sort & sort); | ||
|
|
||
| /** Creates a parameter and stores it in the scoped data-structure | ||
| * arg_param_map_ | ||
| * parameters are variables to be bound by a quantifier | ||
| * @param name the name of the parameter | ||
| * @param sort the sort of the parameter | ||
| * @return the parameter | ||
| */ | ||
| Term create_param(const std::string & name, const smt::Sort & sort); | ||
|
|
||
| /** Declare a let binding mapping a symbol to a term | ||
| * for the current scope | ||
| * @param sym the symbol | ||
| * @param term the term | ||
| */ | ||
| void let_binding(const std::string & sym, const smt::Term & term); | ||
|
|
||
| protected: | ||
| yy::location location_; | ||
|
|
||
| smt::SmtSolver solver_; | ||
|
|
||
| std::unordered_map<std::string, smt::Term> | ||
| all_symbols_; ///< remembers all symbolic constants | ||
| ///< and functions | ||
| ///< even after context is popped | ||
|
|
||
| UnorderedScopedSymbolMap | ||
| global_symbols_; ///< symbolic constants and functions | ||
| ///< defined functions with no arguments | ||
| ///< scoped by the solver context | ||
| ///< e.g. push / pop | ||
|
|
||
| UnorderedScopedSymbolMap | ||
| arg_param_map_; ///< map for arguments (to define-funs) | ||
| ///< and parameters (bound variables) | ||
| ///< scoped by the term structure | ||
| ///< e.g. nested quantifiers | ||
|
|
||
| // define-fun data structures | ||
| std::unordered_map<std::string, smt::Term> | ||
| defs_; ///< keeps track of define-funs | ||
| std::unordered_map<std::string, smt::TermVec> | ||
| def_args_; ///< keeps track of define-fun | ||
| ///< arguments | ||
| std::unordered_map<smt::Sort, smt::TermVec> | ||
| tmp_args_; ///< temporary variables | ||
| ///< organized by sort | ||
| std::vector<std::unordered_map<smt::Sort, size_t>> | ||
| sort_arg_ids_; ///< scope-dependent argument ids in use | ||
| ///< example: sort_arg_ids_.back()[intsort] | ||
| ///< returns the first index into tmp_args | ||
| ///< (might be out of bounds, which means a new | ||
| ///< tmp argument is needed) | ||
| ///< that is currently unused in this scope | ||
|
|
||
| // useful constants | ||
| std::string def_arg_prefix_; ///< the prefix for renamed define-fun arguments | ||
| }; | ||
|
|
||
| } // namespace smt |
Oops, something went wrong.