Model-based theory combination
AssigneeMicrosoft Corporation
InventorsLeonardo M. de Moura, Nikolaj S. Bjorner
Life of this patent
Estimating the term…
Abstract
A method is described for combining models of a plurality of theory solvers in order to produce a model which may be satisfiable by each of the plurality of theory solvers. A model is accessed for a first theory solver which is satisfiable in the first theory solver. It is determined that one or more equalities are implied by the model and it is determined if the equalities are compatible with a second solver. The model is updated in accordance any equalities determined not to be compatible with the second solver. A method is also described for mutation of models using freedom intervals. A freedom interval is determined for a variable within a model and the model is updates by choosing a value for the variable which lies within the freedom interval.
Claims20
In a computing environment comprising at least one processor operatively coupled to system memory, a method for combining the models of a plurality of theory solvers in order to produce a model which is satisfiable by each of the plurality of theory solvers, the method comprising:
- a processor accessing a model for a first theory solver which is satisfiable in the first theory solver;
- the processor determining a set of one or more equalities which are implied by the model, comprising determining that each equality in the set of one or more equalities include a plurality of symbols that have the same value in the model;
- the processor determining that at least one of the set of one or more equalities are not compatible with a second theory solver, comprising communicating one or more equalities from the set of one or more equalities to the second theory solver;
- and
- the processor updating the model in accordance with at least one equality determined not to be compatible with the second solver to create an updated model, wherein updating comprises backtracking to fix values assigned in the model which imply equalities which are not compatible with the second theory solver, such that the updated model is satisfiable in both the first theory solver and the second theory solver.
One or more physical computer storage media having stored thereon computer-executable instructions which, when executed by one or more computer processors, perform a method for combining the models of a plurality of theory solvers in order to produce a model which is satisfiable by each of the plurality of theory solvers, the method comprising:
- a computer system accessing a model for a first theory solver which is satisfiable in the first theory solver, the computer system including the one or more computer processors;
- the computer system determining a set of one or more equalities which are implied by the model, comprising determining that each equality in the set of one or more equalities include a plurality of symbols that have the same value in the model;
- the computer system determining that one of the set of one or more equalities are not compatible with a second theory solver, comprising communicating one or more equalities from the set of one or more equalities to the second theory solver;
- and
- the computer system updating the model in accordance with the one or more equalities determined not to be compatible with the second solver to create an updated model wherein updating comprises backtracking to fix values assigned in the model which imply equalities which are not compatible with the second theory solver, such that the updated model is satisfiable in both the first theory solver and the second theory solver.
A computer system comprising:
- one or more processors;
- and
- one or more storage media having stored computer-executable instructions that, when executed by the one or more processors, cause the computer system to perform a method, comprising:
- the computer system accessing a model for a first theory solver which is satisfiable in the first theory solver;
- the computer system determining a set of one or more equalities which are implied by the model, comprising determining that each equality in the set of one or more equalities include a plurality of symbols that have the same value in the model;
- the computer system determining that one of the set of one or more equalities are not compatible with a second theory solver, comprising communicating one or more equalities from the set of one or more equalities to the second theory solver;
- and
- the computer system updating the model in accordance with the one or more equalities determined not to be compatible with the second solver to create an updated model, wherein updating comprises backtracking to fix values assigned in the model which imply equalities which are not compatible with the second theory solver, such that the updated model is satisfiable in both the first theory solver and the second theory solver.
Dependencies are inferred from the claim text.